Блог

Я экспериментирую с возможностью встраивания доказательств HOL4 в Coq.

В HOL можно дать такое определение, как

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

Можно ли каким-то образом определить эту функцию в Coq аналогичным образом? Моя попытка не удалась на последней строке из-за

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

Код:

 Axiom EQ : forall {aa:Type}, aa -gt; aa -gt; 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) -gt; (t2 == t3) -gt; (t1 == t3). Definition ALPHA t1 t2 := TRANS (REFL t1) (REFL t2).  

добавлен: Может быть, существует такой метод определения АЛЬФА, чтобы мы могли предположить, что t1=t2? (Я имею в виду действительно, в стандартном смысле равенства Кока). Я не могу добавить предположение (H:t1=t2), но тогда мне нужно как-то сопоставить. Как выполнить сопоставление с равенством?

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

Можете ли вы подробнее рассказать о том, как это определение должно работать в HOL? Если я правильно догадываюсь, ALPHA должна ли быть вещь, которая не проверяет тип, если ее аргументы не являются альфа-конвертируемыми? В Coq вы можете использовать

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

Вы также могли бы сделать

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

или

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

Затем вы можете написать что-то вроде Check ALPHA foo bar того, чтобы посмотреть, являются ли две вещи конвертируемыми. Но я не думаю, что это будет полезно в большинстве ситуаций. Если вы ищете тактическое программирование, возможно, вы ищете unify тактику или constr_eq тактику?

В качестве альтернативы, если вы хотите, чтобы ваше match заявление сработало, вы можете написать

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

Это не проблема унификации, это действительно проблема типизации. REFL t1 имеет тип t1 == t1 и REFL t2 имеет тип t2 == t2 , как указано в сообщении об ошибке. Транзитивность работала бы только в том случае, если бы каким-то образом t1 и t2 были одинаковыми, но это априори не так.

Возможно, то, что вы написали, не то, что вы думаете, что написали. Если бы мы использовали только t1 , то TRANS (REFL t1) (REFL t1) имеет тип t1 == t1 . Вы ожидали ALPHA t1 t2 , что у вас будет типаж t1 == t2 ? Если это так, то ваши EQ отношения были бы тотальными.