The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

In this case, you should be able to define a function "order" of type:

"forall x y, GS1 x y -> nat"

which satisfies (L):

"forall x y (g h : GS1 x y), order g = order h -> g = h".

The order function can be defined as:

"fun x y =>

   match decpaths_nat x y as z in match z with inl _ => nat | _ => False end -> nat end with

   | inl _ => fun (n:nat) => n

   | inr _ => fun (abs:False) => match abs return nat with end

   end"

(L) can now be proved simply with something like:
"intros x y; unfold order; unfold GS1; destruct (decpaths_nat x y); simpl; auto; intros []."

I did not try it, so it may not work as easily, but I am pretty confident it should not be much harder.

Now, you have to prove that "order (Compo a b) = order b + order a" and that "order (Id x) = 0".

With that you can conclude that "order (Compo g (Id y)) = 0+order g = order g", and thus "Compo g (Id y) = g".

The proof of "order (Compo a b) = order b + order a" might be a little tricky, I did not tried it.

Also, I would add, that I am not very found of the use of terms defined with tactics, when the definition is relevant.

Such terms tend to be quite big, and totally unreadable. Having a "nice" definition of Compo could also help you in your proofs.

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

Thanks Cédric and Adam for your help.

I realise that my example was too simplified

so it could be solved without facing the issue

I have. 

Consider this one, where nat is used instead of True.

I still don't know how to prove the id_R law, even 

with Adam insight. 

Definition GS1 := fun n m => match decpaths_nat n m with

                                 inl _ => nat

                               | inr _ => False end.

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 (e+e').

  - destruct e'.

  - destruct e.

Defined. 

Definition Id x : GS1 x x.

  red. rewrite (decpaths_nat_eq eq_refl).2. exact 0.

Defined.

On Thu, Apr 9, 2015 at 2:32 PM, nicolas tabareau <nicolas.tabareau AT inria.fr> 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'}.

--

Nicolas Tabareau
Researcher at Inria
Ascola Group, Nantes