The Coq mailing list

[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