The Coq mailing list

[Victor Porton <porton AT narod.ru>]

The following (correct) code proves under certain conditions equality of two 
dependent records (of type Foo) with one data field and one condition:

[[[[
Require Import Logic.ProofIrrelevance.

Parameter A : Set.
Parameter B : A -> Prop.

Structure Foo := mkFoo { a : A; b : B a }.

(*Axiom proof_irrelevance: forall (P:Prop), forall (p q:P), p=q.*)

Theorem thm (u v : Foo) : (a u = a v -> u = v).
proof.
  consider x0 such that y0:(B x0) from u.
  consider x1 such that y1:(B x1) from v.
  assume e:(x0=x1).
  claim (forall y:B x1,  mkFoo x0 y0 = mkFoo x1 y). (* generalize *)
  per cases on e.
    suppose it is (refl_equal). (* dependent elim *)
    let y':(B x0).
    thus thesis by (proof_irrelevance _ y0 y'). (* automation sometimes needs 
help *)
  end cases.
  end claim.
  hence thesis.
end proof.
Qed.
]]]]

I tried to generalize this code for the case of two data fields and one 
condition. My theory does not verify however, at [suppose it is (my_eq_refl A 
B).] it does not happen equalizing of variables matched by the same 
meta-variables in my pattern. What is my error?

[[[[
Require Import Logic.ProofIrrelevance.

Parameter A : Set.
Parameter B : Set.
Parameter Cond : A -> B -> Prop.

Structure Foo := mkFoo { a : A; b : B; cond : Cond a b }.

(*Axiom proof_irrelevance: forall (P:Prop), forall (p q:P), p=q.*)

Inductive my_eq (A B:Type) : A*B -> A*B -> Prop :=
    my_eq_refl : forall (x:A) (y:B), (my_eq A B (x,y) (x,y)).

Theorem thm (u v : Foo) : (a u = a v -> b u = b v -> u = v).
proof.
  consider x0, y0 such that cond0:(Cond x0 y0) from u.
  consider x1, y1 such that cond1:(Cond x1 y1) from v.
  assume e1:(x0=x1).
  assume e2:(y0=y1).
  have e0:( (x0,y0) = (x1,y1) ).
  then e:( my_eq A B (x0,y0) (x1,y1) ).
  claim (forall cond:Cond x1 y1,  mkFoo x0 y0 cond0 = mkFoo x1 y1 cond). (* 
generalize *)
  per cases on e.
    suppose it is (my_eq_refl A B).
    let cond':(Cond x0 y0).
    thus thesis by (proof_irrelevance _ cond0 cond'). (* automation sometimes 
needs help *)
  end cases.
  end claim.
  hence thesis.
end proof.
Qed.
]]]]

-- 
Victor Porton - http://portonvictor.org