The Coq mailing list

["anabelcesar anabelcesar" <anabelcesar AT gmail.com>]

Dear Instructors,

I' ve only used Coq for a few months so please forgive my ignorance.

 

I have written the following code in order to relate the equality

with an arrow type, but I have obtained an easy proof

for the lemma trans1 but when I tried a similar proof for

the lemma trans2 a "Cannot solve a second-order unification problem"

error is obtained. Is it possible to proof that lemma?

 

Thanks!

 

Anabel

 

--------------

Variable A:Type.
Variable B:Type.

Variable p: A=B.

Lemma a_b: A -> B.
Proof.
intros.
replace B with A.
exact X.
exact p.
Defined.

Lemma b_a: B -> A.
Proof.
intros.
replace A with B.
exact X.
exact  (sym_eq p).
Defined.

Lemma trans1: forall a:A,  (b_a (a_b a))=a.
Proof.
intro.
unfold b_a.
unfold a_b.
case p.
trivial.
Qed.

Lemma trans2: forall b:B,  (a_b (b_a b))=b.

 

 

Hi
 I've only used Coq for a few months so please forgive my ignorance.
>> > > >
>> > > > I am trying to do some formalization work in Coq and have ran
>> across a
>> > > > problem, the essence of which can be summarized below:
>> > > >
>> > > > I have a type that's dependent on some other type, say nat for
>> example:
>> > > > Record T (a:nat) : Type := { some_field : nat }.
>> > > >
>> > > > I have found that in order to state some theorems I need the
>> following
>> > > > equality definition for T:
>> > > >
>> > > > Inductive T_eq (a:nat) (r1:T a) : forall b:nat, T b -> Prop :=
>> > > > | T_eq_intro : forall (r2:T a), r1 = r2 -> T_eq r1 r2.
>> > > >
>> > > > The intention is that for some r1:T a and r2:T b (where a and b
>> might
>> not
>> > > > be
>> > > > definitionally equal), T_eq r1 r2 iff a = b and r1 = r2.
>> > > > The point is that the only way to construct T_eq is to construct
>> with
>> (r1
>> > > > r2:T a) and a proof of r1 = r2.
>> > > >
>> > > > Which works fine until I want to make use of T_eq, ie what I want
>> is
>> the
>> > > > following theorem:
>> > > >
>> > > > forall (a:nat) (r1 r2:T a), T_eq r1 r2 -> r1 = r2.
>> > > >
>> > > > So if I have a proof of T_eq r1 r2, I want to get back the proof of
>> r1=r2.
>> > > > But I can't seem to prove it.  I look at the elimination rule for
>> T_eq:
>> > > >
>> > > > T_eq_ind =
>> > > > fun (a : nat) (r1 : T a) (P : forall b : nat, T b -> Prop)
>> > > >   (f : forall r2 : T a, r1 = r2 -> P a r2) (b : nat)
>> > > >   (t : T b) (t0 : T_eq r1 t) =>
>> > > > match t0 in (T_eq _ t1) return (P b0 t1) with
>> > > > | T_eq_intro x x0 => f x x0
>> > > > end
>> > > >
>> > > > The return type for the case analysis is (P b0 t1) for some P
>> which,
>> as
>> > > > far
>> > > > as I can see, cannot allow for the return type to be r1=r2, so how
>> do
>> I
>> > > > get
>> > > > back the proof of r1=r2?
>> > > >
>> > > > Thanks in advance.