Я пытаюсь доказать это:
Lemma eq_eq: forall (U: Type) (p: U) (eqv: p = p), eq_refl = eqv.
Но, похоже, просто нет способа сделать это. Проблема в том, что тип p = p
равен на одном и том же члене, а затем пытается найти соответствие его экземпляру. Если бы это было не так, достаточно легко доказать, что термин типа с одним конструктором равен этому конструктору.
Lemma eq_tt: forall (U: Type) (x: unit), tt = x.
Proof
fun (U: Type) (x: unit) =>
match x as x'
return tt = x'
with tt => eq_refl
end.
Но когда вы пытаетесь использовать ту же стратегию в моей проблеме, это терпит неудачу.
Lemma eq_eq: forall (U: Type) (p: U) (eqv: p = p), eq_refl = eqv.
Proof
fun (U: Type) (p: U) (eqv: p = p) =>
match eqv as e
in _ = p'
return eq_refl = e
with eq_refl => eq_refl
end.
Это терпит неудачу с Термин "e" имеет тип "p = p", в то время как ожидается, что он будет иметь тип "p = p" (не может объединить "p" "и "p").
Проблема в том, что здесь выражение return
внутренне переводит в функцию предиката что-то вроде этого:
fun (p': U) (e: p = p') =>
eq_refl = e
, которая не может проверить тип, потому что мы имеем теперь потерял ограничение между двумя членами в равенстве e
и eq_refl
требует этого ограничения.
Есть ли способ обойти эту проблему? Я что-то упустил?