The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Current example is solved by 'reflexivity', but perhaps you are looking for 'destruct a,b'.

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva

On Mon, Feb 29, 2016 at 2:09 PM, Kiarash Rahmani <rahmank AT purdue.edu> wrote:

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