证明依赖类型实例之间的相等性 [英] Proving equality between instances of dependent types

问题描述

当尝试形式化与代数结构相对应的类（例如所有等分体的类）时，自然的设计是创建类型 monoid（a：Type）作为对所有必填字段建模的产品类型（元素 e：a ，运算符 app：a-> a-> a ，证明是否满足等边定律等）。为此，我们正在创建地图 monoid：类型->键入。这种方法的可能缺点是，给定一个mono元集 m：monoid a （支持类型 a 的mono集）和 m'：monoid b （具有支持类型 b 的单面体），我们甚至不能写等式 m = m'（更不用说证明了），因为它类型错误。另一种设计是创建类型 monoid ，其中支持类型只是另一个字段 a：Type ，这样给定 m m'：monoid ，询问 m = m'总是有意义的。有人想说，如果 m 和 m'具有相同的支持（ am = am ）且运算符相等（ app m = app m'，这可能要归功于一些扩展的相等公理），以及证明字段无关紧要（因为我们有一些证明无关公理）等，则 m = m'。不幸的是，我们无法事件表示等式 app m = app m'，因为它的类型错误...

When attempting to formalize the class which corresponds to an algebraic structure (for example the class of all monoids), a natural design is to create a type monoid (a:Type) as a product type which models all the required fields (an element e:a, an operator app : a -> a -> a, proofs that the monoid laws are satisfied etc.). In doing so, we are creating a map monoid: Type -> Type. A possible drawback of this approach is that given a monoid m:monoid a (a monoid with support type a) and m':monoid b (a monoid wih support type b), we cannot even write the equality m = m' (let alone prove it) because it is ill-typed. An alternative design would be to create a type monoid where the support type is just another field a:Type, so that given m m':monoid, it is always meaningful to ask whether m = m'. Somehow, one would like to argue that if m and m' have the same supports (a m = a m) and the operators are equals (app m = app m', which may be achieved thanks to some extensional equality axiom), and that the proof fields do not matter (because we have some proof irrelevance axiom) etc. , then m = m'. Unfortunately, we can't event express the equality app m = app m' because it is ill-typed...

为简化问题，假设我们有：

To simplify the problem, suppose we have:

Inductive myType : Type :=
| make : forall (a:Type), a -> myType.
.

我希望得到以下形式的结果：

I would like to have results of the form:

forall (a b:Type) (x:a) (y:b), a = b -> x = y -> make a x = make b y.

此语句的类型错误，因此我们无法使用它。

This statement is ill-typed so we can't have it.

我也许有公理可以证明 a 和 b两种类型是相同的，我也许可以证明 x 和 y 的确也相同，但我想拥有一个工具，使我可以得出结论： make ax = make by 。任何建议都欢迎。

I may have axioms allowing me to prove that two types a and b are same, and I may be able to show that x and y are indeed the same too, but I want to have a tool allowing me to conclude that make a x = make b y. Any suggestion is welcome.

推荐答案

一种低技术的方法来证明这一点，即使用提供的相等性插入手动类型转换。也就是说，您没有假设 x = y ，而是有了假设（CAST q x）= y 。在下面，我明确地将强制类型转换写为匹配项，但是您也可以通过定义一个函数来使其看起来更好。

A low-tech way to prove this is to insert a manual type-cast, using the provided equality. That is, instead of having an assumption x = y, you have an assumption (CAST q x) = y. Below I explicitly write the cast as a match, but you could also make it look nicer by defining a function to do it.

Inductive myType : Type :=
| make : forall (a:Type), a -> myType.

Lemma ex : forall (a b:Type) (x:a) (y:b) (q: a = b), (match q in _ = T return T with eq_refl => x end) = y -> make a x = make b y.
Proof.
  destruct q.
  intros q.
  congruence.
Qed.

有一种更好的方法可以通过使用异构相等来隐藏大多数这种机制。 JMeq。我建议 CPDT的平等一章进行详细介绍。您的示例变为

There is a nicer way to hide most of this machinery by using "heterogenous equality", also known as JMeq. I recommend the Equality chapter of CPDT for a detailed introduction. Your example becomes

Require Import  Coq.Logic.JMeq.

Infix "==" := JMeq (at level 70, no associativity).

Inductive myType : Type :=
| make : forall (a:Type), a -> myType.

Lemma ex : forall (a b:Type) (x:a) (y:b), a = b -> x == y -> make a x = make b y.
Proof.
  intros.
  rewrite H0.
  reflexivity.
Qed.

通常，尽管可以在没有公理的情况下证明这个特定定理，但是如果您采用这种形式的形式化没有平等的公理，您很可能会遇到无法在Coq中证明的目标。特别是，这种依存记录的内插性是无法证明的。 JMEq库将自动使用关于异构相等的公理 JMeq_eq ，这非常方便。

In general, although this particular theorem can be proved without axioms, if you do the formalization in this style you are likely to encounter goals that can not be proven in Coq without axioms about equality. In particular, injectivity for this kind of dependent records is not provable. The JMEq library will automatically use an axiom JMeq_eq about heterogeneous equality, which makes it quite convenient.

这篇关于证明依赖类型实例之间的相等性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！