The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The key to this proof is that the equality you're matching on must take the form of [0 = z] for any [z : nat].  The insight is that it's possible to generalize [nil] to a term of type [t (option nat) z] that is judgmentally [nil] when [z] is judgmentally 0 (what it is on the other values of [z] is irrelevant).

On Fri, May 29, 2015 at 5:13 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Here's a shorter, more ad-hoc, proof:

Require Import Vector.

Require Import ArithRing.

Goal match mult_n_O 0 in (_ = y) return (t (option nat) y) with

   | eq_refl => nil (option nat)

   end = nil (option nat).

Proof.

  generalize (mult_n_O 0).

  simpl.

  set (z := 0) at 2.

  change (nil (option nat)) with (Vector.const (@None nat) z) at 2.

  change 0 with z at 2.

  clearbody z.

  intros []; reflexivity.

Defined.

On Fri, May 29, 2015 at 3:53 PM, Amin <amintimany AT gmail.com> wrote:

Oh wait, It seems I haven’t been paying close enough attention. In this case as e is equality over type nat, UIP does in fact hold for it (as equality for nat is decidable) and thus we can prove this lemma as follows:

Require Import Vector.

Require Import ArithRing.

Require Import Coq.Logic.JMeq.

Require Import Coq.Arith.Peano_dec.

Program Fixpoint ScatHUnion_0 {A} {n:nat} (pad:nat): t A n -> t (option A) ((S pad)*n) :=

 match n return (t A n) -> (t (option A) ((S pad)*n)) with

 | 0 => fun _ => @nil (option A)

 | S p => fun a => cons _ (Some (hd a)) _ (append (const None pad) (ScatHUnion_0 pad (tl a)))

 end.

Next Obligation.

 ring.

Defined.

(* code from EqFacts.v in the gist link in the other email *)

Section Eq_Facts.

  Variable A : Type.

 

  Definition K := forall (x : A) (P : x = x -> Prop), P eq_refl -> forall (eq : x = x), P eq.

 

  Definition URIP := forall (x : A) (eq : x = x), eq = eq_refl.

 

  Definition UIP := forall (x y : A) (eq eq' : x = y), eq = eq'.

 

  Definition eq_rect_eq := forall (x : A) (P : A -> Type) (eq : x = x) (p : P x), p = eq_rect x P p x eq.

 

  Definition projT2_eq := forall (x : A) (P : A -> Type) (p q : P x), existT P x p = existT P x q -> p = q.

 

  Lemma K_URIP : K -> URIP.

  Proof.

    intros k x eq. 

    apply (k _ (fun p => p = eq_refl) eq_refl).

  Qed.

 

  Lemma UIP_UIP : URIP -> UIP.

  Proof.

    intros urip x y eq eq'. 

    destruct eq'.

    apply urip.

  Qed.

 

  Theorem UIP_eq_rect_eq : UIP -> eq_rect_eq.

  Proof.

    intros uip x P eq p.

    rewrite (uip _ _ eq eq_refl); trivial.

  Qed.    

 

  Theorem eq_rect_eq_projT2_eq : eq_rect_eq -> projT2_eq.

  Proof.

    intros ere x P p q H.

    set (proj1_eq := fun (v : sigT P) (H : existT P x p = v) => match H in _ = z return projT1 (existT P x p) = projT1 z with eq_refl => eq_refl end).

    assert (H' : match (proj1_eq (existT P x q) H) in _ = u return P u with eq_refl => projT2 (existT P x p) end = projT2 (existT P x q)).

    {

      destruct H; trivial.

    }

    cbv in ere.

    rewrite <- (ere _ _ (proj1_eq _ H)) in H'; trivial.

  Qed.    

 

  Theorem projT2_eq_k : projT2_eq -> K.

  Proof.

    intros p2 x P H eq.

    cut (eq = eq_refl); [intros H'; rewrite H'; trivial|].

    apply p2; destruct eq; trivial.

  Qed.

 

  Section Dec.

    Hypothesis A_dec : forall a b : A, {a = b} + {a <> b}.

 

    Definition make_eq {a b : A} (eq : a = b) : a = b.

    Proof.

      destruct (A_dec a b) as [H|H].

      + exact H.

      + exact (False_rect _ (H eq)).

    Defined.

 

    Theorem make_eq_const : forall {a b : A} (eq eq' : a = b), make_eq eq = make_eq eq'.

    Proof.

      intros a b eq eq'.

      cbv.

      destruct A_dec as [H|H]; trivial.

      destruct (H eq).

    Qed.

 

    Theorem make_eq_com_sym : forall {a b : A} (eq : a = b), eq_trans (eq_sym (make_eq (eq_refl a))) (make_eq eq) = eq.

    Proof.

      intros a b eq.

      destruct eq.

      destruct (make_eq eq_refl); trivial.

    Qed.    

 

    Theorem k : K.

    Proof.

      intros x P H eq.

      rewrite <- make_eq_com_sym in H.

      rewrite <- make_eq_com_sym.

      replace (make_eq eq) with (make_eq (eq_refl x)); trivial.

      apply make_eq_const.

    Qed.

  End Dec.

End Eq_Facts.

(* End of code from EqFacts.v *)

Lemma URIP_nat : URIP nat.

Proof.

  apply K_URIP.

  apply k.

  apply eq_nat_dec.

Qed.

Lemma test0: @ScatHUnion_0 nat 0 0 (@nil nat) = (@nil (option nat)).

Proof.

  cbv.

  generalize (mult_n_O 0); intros e.

  cbn in e.

  rewrite (URIP_nat 0 e).

  trivial.

Qed.

On 29 May 2015, at 21:34, Amin <amintimany AT gmail.com> wrote:

Hi,

This lemma is in fact (without help of some axioms) not provable in Coq. That said, here is a solution that uses an axiom (JMeq_eq). I explain the problem below. 

Require Import Vector.

Require Import ArithRing.

Require Import Coq.Logic.JMeq.

Program Fixpoint ScatHUnion_0 {A} {n:nat} (pad:nat): t A n -> t (option A) ((S pad)*n) :=

 match n return (t A n) -> (t (option A) ((S pad)*n)) with

 | 0 => fun _ => @nil (option A)

 | S p => fun a => cons _ (Some (hd a)) _ (append (const None pad) (ScatHUnion_0 pad (tl a)))

 end.

Next Obligation.

 ring.

Defined.

Lemma test0: @ScatHUnion_0 nat 0 0 (@nil nat) = (@nil (option nat)).

Proof.

  cbv.

  generalize (mult_n_O 0); intros e.

  cbn in e.

(*

At this point you will have:

  e : 0 = 0

  ============================

   match e in (_ = y) return (t (option nat) y) with

   | eq_refl => nil (option nat)

   end = nil (option nat)

As you see the problem now would be solved if we could just replace e with eq_refl (i.e., destruct e.)

This is impossible though. This is because doing a case analysis on e would require us to consider

the general case where e is replaced by e’ : 0 = x for a general x. This on the other makes the goal

ill-typed.

The problem boils down to the fact that in coq you can’t prove unicity of identity proofs (or any other axiom equivalent

to it, e.g., JMeq_eq I used).

Using JMeq_eq changes eq to JMeq which due to its heterogeneity does not become ill-typed under

such an abstraction as above.

*)

  apply JMeq_eq.

  destruct e.

  trivial.

Qed.

Here is a short Coq script proving equivalence of some axioms that are equivalent to UIP (unicity of identity proof) and JMeq_eq:

https://gist.github.com/amintimany/798a096e2f2ff0582b36

Regards,

Amin

On 29 May 2015, at 20:21, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

I am wondering what is a good approach to trying to prove some things like this:

Require Import Vector.
Require Import ArithRing.

Program Fixpoint ScatHUnion_0 {A} {n:nat} (pad:nat): t A n -> t (option A) ((S pad)*n) :=
 match n return (t A n) -> (t (option A) ((S pad)*n)) with
 | 0 => fun _ => @nil (option A)
 | S p => fun a => cons _ (Some (hd a)) _ (append (const None pad) (ScatHUnion_0 pad (tl a)))
 end.
Next Obligation.
 ring.
Defined.

(This definition works only under Coq 8.5. Under 8.4 I had to define it differently).
I stuck proving the following trivial lemma:

Lemma test0: @ScatHUnion_0 nat 0 0 (@nil nat) = (@nil (option nat)).

I could not get much further than:

test0 < compute.
1 subgoal

 ============================
  match mult_n_O 0 in (_ = y) return (t (option nat) y) with
  | eq_refl => nil (option nat)
  end = nil (option nat)

Any suggestions how to deal with proving constructs like this?
Thanks!

Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva