The Coq mailing list

[Frederic Blanqui <blanqui AT lri.fr>]

On Tue, 21 Sep 1999, Claudio Sacerdoti Coen wrote:

> I need something like this:
> 
> Inductive equal1 : (A:Type)(B:Type) A -> B -> Prop :=
>  eq1 : (A:Type)(B:Type)(a:A)(b:B)(A==B)->(a==b)->(equal1 A B a b).
> 
> But this fails to typecheck, because a and b are of different types.
> But if (A==B) then I expect (a == b) to typecheck (perhaps B should
> be automatically coerced to A).

This is normal since A and B have not the same normal form (they are
distinct variables).

If you look at the following example, you will see that terms with the 
same normal forms are identified, hence are equal through the Leibniz
equality (eq or = in Coq).

Inductive list[A:Set]: nat->Set :=
  nil: (list A O)
  | cons: A->(n:nat)(list A n)->(list A (S n)).

Fixpoint app[A:Set; n1:nat; l1:(list A n1)]: (n2:nat)(list A n2)
    ->(list A (plus n1 n2)) := [n2:nat; l2:(list A n2)]
  <[n1:nat][l1:(list A n1)](list A (plus n1 n2))>Cases l1 of
    nil => l2
    | (cons x n l) => (cons A x (plus n n2) (app A n l n2 l2))
  end.

In the first branch, the type is (list A n2) while the result should be
(list A (plus n1 n2)). But, in this case, as l1, which is of type (list A
n1), matches nil, it must also be of type (list A O). Hence, n1=O and
(plus n1 n2) reduces to n2. Note that it depends on the way plus has been
defined: by induction on the first or on the second argument...

> If I define an inductive type as
> 
> Inductive T : Type := c : (A:Type) A -> T.
> 
> then this is another way of defining equal1:
> 
> Definition equal1 := [A:Type][B:Type][a:A][b:B](c A a)==(c B b).
> 
> But if I try:
> 
> Goal (eq1 nat nat O (S O))->False.
>  Intros ; Unfold eq1 in H ; Discriminate.

Here, I think you mean equal1 instead of eq1.

> I get
> 
> Uncaught exception: File "equality.ml", line 0, characters 20213-20225:
> Assertion failed
> If this is in user-written tactic code, then it needs to be modified.
> If this is in system code, then
> it needs to be reported.

I think it is due to the fact that the tactics Discriminate or Injection
have been defined on = and not on ==.

Frederic Blanqui.

------------------------------------------------------------------------------
Laboratoire de Recherche en Informatique (LRI) - Equipe DEMONS
batiment 490, bureau 153, Universite Paris-Sud 91405 ORSAY (FRANCE)
tel:33.1.69.15.42.35 - fax:33.1.69.15.65.86 - web:http://www.lri.fr/~blanqui