Доказательство с круговой симметрией в Coq - PullRequest
Новая
       26

Доказательство с круговой симметрией в Coq

0 голосов
/ 30 августа 2018

Я работаю над доказательством, использующим структурную конгруэнцию, которая определена очень похоже на этот пример: 

Require Import Nat.
Require Import Omega.

Inductive expr :=
  | Const : nat -> expr
  | Add : expr -> expr -> expr.


Reserved Notation "e1 === e2" (at level 80).
Inductive expr_congruence : expr -> expr -> Prop :=
  | Commutative : forall e1 e2, Add e1 e2 === Add e2 e1
  | Associative : forall e1 e2 e3, Add (Add e1 e2) e3 === Add e1 (Add e2 e3)
  | CongruenceReflexive : forall e, e === e
  | CongruenceSymmetric : forall e1 e2, e1 === e2 -> e2 === e1
  | CongruenceTransitive :
      forall e1 e2 e3, e1 === e2 -> e2 === e3 -> e1 === e3
  where "e1 === e2" := (expr_congruence e1 e2).

Я сталкиваюсь с проблемами при попытке определить что-то в форме forall e1 e2, e1 === e2 -> P e1 -> P e2: я всегда получаю круговую логику. Как пример: 

Inductive is_zero : expr -> Prop :=
  | ZConst : is_zero (Const 0)
  | ZAdd : forall e1 e2, is_zero e1 -> is_zero e2 -> is_zero (Add e1 e2).

Hint Constructors is_zero expr_congruence.

Lemma is_zero_over_congruence :
  forall e1 e2,
    e1 === e2 ->
    is_zero e1 ->
    is_zero e2.
Proof.
  induction 1; eauto; intros.

  Show 3.
(**
1 subgoal
e1, e2 : expr
H : e1 === e2
IHexpr_congruence : is_zero e1 -> is_zero e2
H0 : is_zero e2
**)

Единственная связь между e1 и e2 здесь заключается в том, что они совпадают. Инверсия или наведение на них в конечном итоге приводит к тому же случаю, который не дает никакой дополнительной информации.

Как правильно обращаться с индукцией при использовании структур с симметрией, определенной таким образом?

1 Ответ

0 голосов
/ 30 августа 2018

По крайней мере, в этом минимальном примере вам просто нужно доказать что-то более сильное: 

Lemma is_zero_over_congruence :
  forall e1 e2, e1 === e2 -> is_zero e1 <-> is_zero e2.
Proof.
  induction 1.
  - split; intros HI; inversion HI; eauto.
  - split; intros HI; inversion HI; [inversion H1 | inversion H2]; eauto.
  - reflexivity.
  - symmetry. auto.
  - rewrite IHexpr_congruence1, IHexpr_congruence2. reflexivity.
Qed.

так что вы можете использовать is_zero e1 <-> is_zero e2 в качестве индуктивной гипотезы, когда вам нужно доказать is_zero e2 <-> is_zero e1.

...