Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Equality in the assumptions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Equality in the assumptions


Chronological Thread 
  • 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.

Top of Page