The Coq mailing list

[Amin <amintimany AT gmail.com>]

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