时间戳

首页 > 解决方案 > 如何在 Coq 中推广方程两边的变量？

coq - 如何在 Coq 中推广方程两边的变量？

问题描述

我有这个目标

size (flatten (N t1 t2)) = size (N t1 t2)

N是一个bin构造函数，我怎样才能N t1 t2在两边替换t3 : bin？

我的假设是

t1, t2 : bin
IHt1 : size (flatten t1) = size t1
IHt2 : size (flatten t2) = size t2

如果我可以重写size (flatten (N t1 t2)) = size (N t1 t2)，size (flatten t3) = size t3那么我可以应用我的假设来完成证明。

这是完整的代码

Require Import Nat.
Require Import Arith.

Inductive bin : Type :=
    L : bin
  | N : bin -> bin -> bin.

Fixpoint flatten_aux (t1 t2 : bin) : bin :=
  match t1 with
    L => N L t2
  | N t'1 t'2 => flatten_aux t'1  (flatten_aux t'2 t2)
  end.

Fixpoint flatten (t : bin) : bin :=
  match t with
    L => L
  | N t1 t2 => flatten_aux t1 (flatten t2)
  end.

Fixpoint size (t : bin) : nat :=
  match t with
    L => 1
  | N t1 t2 => 1 + size t1 + size t2
  end.


Lemma flatten_aux_size :
  forall t1 t2, size (flatten_aux t1 t2) =
    size t1 + size t2 + 1.
  induction t1.
  { intros t2.
    simpl.
    ring.
  }
  { intros t2; simpl.
    rewrite IHt1_1.
    rewrite IHt1_2.
    ring.
  }
Qed.

Lemma flatten_size : forall t, size (flatten t) = size t.
  induction t.
  { trivial.
  }
  { simpl.
    (* goal size (flatten (N t1 t2)) = size (N t1 t2) *)

最后我使用这个解决方案

Lemma flatten_size : forall t, size (flatten t) = size t.
  induction t.
  { trivial.
  }
  { simpl.
    rewrite flatten_aux_size.
    rewrite <- IHt1.
    rewrite <- IHt2.
    rewrite Nat.add_comm.
    simpl.
    reflexivity.
  }
Qed.

标签： coq

解决方案

你为什么会有size (flatten t3) = size t3？你的假设不是普遍量化的，size (flatten t2) = size t2适用于那个特定的t2（与 相同t1）。如果没有更多细节，我们无法为您提供帮助，但我希望您更愿意展示flatten应用时的行为N t1 t2方式，flatten t1然后flatten t2帮助您得出结论。

推荐阅读