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
- [Coq-Club] Equality in the assumptions, Kiarash Rahmani, 02/29/2016
Archive powered by MHonArc 2.6.18.