The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-04-09 14:32 GMT+02:00 nicolas tabareau <nicolas.tabareau AT inria.fr>:

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

​I would start by proving the following:

"forall x y (g h : GS1 x y), g = h"

As we know, "GS1 x y" either reduces to "True" or to "False", thus this equality should be provable.

Once you have it, "Compo e (Id y)" and "e" are both of type "GS1 x y", and thus are equal.

So the question is how to prove the first lemma.

First introduce x and y, then unfold GS1. You should have:

"forall (g h : match decpaths_nat x y with … end), g = h."

From here, simply "case/destruct/whatever_elimination_principle (decpaths_nat x y)", and you end up with the following two subgoals to prove:

"forall (g h : True), g = h"

"forall (g h : False), g = h"

both of them are solvable with "intros [] []; split." (in fact, "intros []." is enough for the second goal).

​