coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Kiarash Rahmani <rahmank AT purdue.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Equality in the assumptions
Date: Mon, 29 Feb 2016 22:09:12 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=rahmank AT purdue.edu; spf=None smtp.mailfrom=rahmank AT purdue.edu; spf=Pass smtp.helo=postmaster AT na01-bl2-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:rlo64BMMSBxDOyrPoM4l6mtUPXoX/o7sNwtQ0KIMzox0KPr6rarrMEGX3/hxlliBBdydsKIbzbSG+Pm9AyQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTokb7isMSOOU1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvNa8/VPlTCCksG2Ez/szi8xfZB0Pb7XwFF24SjxBgAg7f7Ri8UI2n4QXgse8o+yiTJ8TtTfgOUDSn5qFqAEvygScCPjg62HnKkMBtgeRWrA/39E83+JLdfIzAbKk2RajaZ95PHWc=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:23

Hey all,

I am stuck in the middle of a proof.

In assumptions, I have an equality of two inductively defined propositions, and I need to make use of it. Here is a toy example to explain it:

Inductive my_type : Type :=

| one : my_type

| two : my_type

| other : nat -> my_type.

Inductive my_ind (a b:my_type) : my_type -> Prop :=

| cons_introl :forall x: my_type, b = one -> my_ind a b x

| cons_intror :forall x: my_type, a = one -> my_ind a b x.

Theorem my_theorem:forall (a b c: my_type), (my_ind a b) = (my_ind b c) -> 2=2.

Proof.

intros a b c H.

(*How sould I make use of H? inversion, injection, unfold, does not seem to work*)

(*I need to destruct two possible ways of constructing my_ind, and then prove the goal in each case*)

Abort.

Thank you very much