The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Here's another solution.  It applies the general idea of generalizing 
over proof terms from the goal, when the types of those proof terms 
mention the term you want to [destruct].

Ltac contra :=
  match goal with
  | [ H : _ |- _ ] => destruct H; solve [ auto ]
  end.

Lemma True_irrel : forall pf1 pf2 : True, pf1 = pf2.
Proof.
  destruct pf1, pf2; auto.
Qed.

Definition Id_R x y : forall (e:GS1 x y), Compo e (Id y) = e.
  unfold GS1, Compo. simpl.

  generalize (@decpaths_nat_eq x y).
  destruct (decpaths_nat x y); intros; try contra.
  apply True_irrel.
Qed.


On 04/09/2015 08:32 AM, nicolas tabareau wrote:
> Hi,
>
> I have difficulty in proving equality on terms of a
> dependent type that uses pattern matching.
>
> Here is a simplified example (that works with
> the code given at the end of the mail).
>
> I start by defining a type depending on two naturals,
> which is True when they are equal and false otherwise.
>
> Definition GS1 := fun n m => match decpaths_nat n m with
>                                  inl _ => True
>                                | inr _ => False end.
>
> I can defined a kind of composition and identity.
>
> Definition Compo {x y z} : GS1 x y -> GS1 y z -> GS1 x z.
>   intros e e'. unfold GS1 in *.
>   destruct (decpaths_nat x y). destruct (decpaths_nat y z).
>   - rewrite (decpaths_nat_eq (e0 @ e1)).2. exact I.
>   - destruct e'.
>   - destruct e.
> Defined.
>
> Definition Id x : GS1 x x.
>   red. rewrite (decpaths_nat_eq eq_refl).2. exact I.
> Defined.
>
> But then, I am not able to prove a simple identity law
> (at least by trying to use the pattern matching directly)
>
> Definition Id_R x y : forall (e:GS1 x y), Compo e (Id y) = e.
>   (* does not work *)
>   unfold GS1, Compo. simpl.
>   destruct (decpaths_nat y y).
>
> Can anyone help me  ?
>
> Thanks,
>
> -- Nicolas
>
>
> (* some code to be used with the example above  *)
>
> Notation "x .1" := (projT1 x) (at level 3).
> Notation "x .2" := (projT2 x) (at level 3).
>
> Inductive Empty : Type.
>
> Definition not (T : Type) := T -> Empty.
>
> Notation "~~ A" := (not A) (at level 75).
>
> Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z.
>   destruct p; exact q.
> Defined.
>
> Notation "p @ q" := (concat p q) (at level 20) : type_scope.
>
> Parameter decpaths_nat : forall (x y : nat), (x = y) + ~~ (x = y).
>
> Parameter decpaths_nat_eq : forall {g g'} (e: g = g'),
>                               {e' : g = g' & decpaths_nat g g' = inl e'}.
>
> Parameter decpaths_nat_neq : forall {g g'} ( e : ~~ g = g'),
>                                {e' : ~~ g = g' & decpaths_nat g g' = 
> inr e'}.