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*)
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.