CODEWITHSUNDEEP
coqhol
g_d
g_d

Reputation: 707

Unification problem with HOL-style alpha-conversion in Coq (matching the equality)

I am experimenting with possibility of embedding of HOL4 proofs in Coq.

In HOL it is possible to give definition like

fun ALPHA t1 t2 = TRANS (REFL t1) (REFL t2)

Is it possible to somehow define this function in Coq in similar way? My attempt fails on the last line due to

The term "REFL t2" has type "t2 == t2"
while it is expected to have type "t1 == ?t3" (cannot unify 
"t2" and "t1").

The code:

Axiom EQ : forall {aa:Type}, aa -> aa -> Prop.
Notation " x == y " := (@EQ _ x y)  (at level 80).
Axiom REFL : forall {aa:Type} (a:aa), a == a.
Axiom TRANS :forall {T:Type}{t1 t2 t3:T},
 (t1 == t2) -> (t2 == t3) -> (t1 == t3).
Definition ALPHA t1 t2 := TRANS (REFL t1) (REFL t2).

ADDED: Maybe there is a method of defining ALPHA such that we can assume that t1=t2? (I mean indeed, in Coq's standard sense of equality). I cann add assumption (H:t1=t2), but then I need to have matching somehow. How to do the matching with equality?

Definition ALPHA (t1 t2:T) (H:t1=t2) : t1==t2 :=
match H with
| eq_refl _ => TRANS (REFL t1) (REFL t2)
end
. (*fails*)

Upvotes: 0

Views: 74

Answers (2)

Jason Gross
Jason Gross

Reputation: 6128

Can you say more about how this definition is supposed to work in HOL? If I'm guessing correctly, ALPHA is supposed to be a thing that fails to typecheck if its arguments are not alpha-convertible? In Coq, you can use

Notation ALPHA t1 t2 := (TRANS (REFL t1) (REFL t2)).

You could also do

Notation ALPHA t1 t2 := (REFL t1 : t1 == t2).

or

Notation ALPHA t1 t2 := (eq_refl : t1 = t2).

Then you can write things like Check ALPHA foo bar to see if two things are convertible. But I don't think this will be useful in most situations. If you're looking for tactic programming, perhaps you're looking for the unify tactic or the constr_eq tactic?

Alternatively, if you want your match statement to work, you can write

Definition ALPHA {T:Type} (t1 t2 : T) (H : t1 = t2) : t1 == t2 :=
  match H with eq_refl => REFL _ end.

Upvotes: 1

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

This is not a unification problem, it really is a typing problem. REFL t1 has type t1 == t1 and REFL t2 has type t2 == t2 as the error message is telling you. Transitivity would only work if somehow t1 and t2 were the same, but this is a priori not the case.

Perhaps what you wrote is not what you think you wrote. If we were using only t1, then TRANS (REFL t1) (REFL t1) has type t1 == t1. Were you expecting ALPHA t1 t2 to have type t1 == t2? If it is the case, then your EQ relation would be total.

Upvotes: 0

Related Questions