0

我无法解决应该使用指称语义的 Coq 定理。如果我从这一点继续前进，我总是陷入无限循环。

在这种情况下应该使用什么策略？我在哪里做错了这个？我应该以不同的方式开始吗？

From Coq Require Import Strings.String
                        Arith.PeanoNat
                        Arith.Plus.

Definition Ident : Type := string.

Inductive AExp : Type :=
| ALit (n : nat)
| AVar (s : Ident)
| APlus (a1 a2 : AExp)
| ADup (n : AExp)
.

Definition State := Ident -> nat.

Definition empty : State := fun x => 0.

Definition aState : State := 
fun x =>
  match x with
  | "X"%string => 1
  | "Y"%string => 2
  | "Z"%string => 42
  | _ => 0
  end
.

Definition X:Ident := "X"%string.
Definition Y:Ident := "Y"%string.
Definition Z:Ident := "Z"%string.

Fixpoint val (a : AExp) (s : State) : nat :=
match a with
| ALit n => n
| AVar x => s x
| APlus a1 a2 => val a1 s + val a2 s
| ADup a => val a s + val a s
end.

Fixpoint aqb (a1 a2 : AExp) : bool :=
match a1, a2 with
| ALit n, ALit m => Nat.eqb n m
| AVar s, AVar x => String.eqb s x
| APlus a1 a2, APlus a1' a2' => aqb a1 a1' && aqb a2 a2'
| ADup a1, ADup a1' => aqb a1 a1'
| _, _ => false
end.

Fixpoint optmal (a : AExp) : AExp :=
match a with
| APlus a1 a2 => 
  if aqb a1 a2
  then ADup (optmal a1)
  else APlus (optmal a1) (optmal a2)
| ADup a0 => ADup (optmal a0)
| _ => a
end.

Theorem optmald :
  forall a s, val a s = val (optmal a) s.
Proof.
intros. unfold val. induction a.
* simpl. reflexivity.
* simpl. reflexivity.
*
4

2 回答 2

0

该定理由对 的归纳得出a。然而，首先证明引理是有用的aeq_val。接下来是归纳a1和考虑和a2的分支是否相等的情况。所有的ing 都可以自动处理，这是一种可以解决许多只需要对等式和自反性进行推理的目标的策略。a1a2rewritecongruence

Lemma aeq_val : forall  a1 a2 s, aqb a1 a2 = true -> val (optmal a2) s = val (optmal a1) s.
  induction a1; destruct a2; simpl; try congruence; intros ? H.
  - apply eq_sym, EqNat.beq_nat_eq, eq_sym, H. 
  - apply eq_sym, f_equal, String.eqb_eq, H.
  - destruct (andb_prop _ _ H) as [H1 H2].
    apply aqb_eq in H1; apply aqb_eq in H2.
    destruct (aqb a2_1 a2_2) eqn:Hx;
      destruct (aqb a1_1 a1_2) eqn:Hy;
      congruence.
  - apply aqb_eq in H; congruence.
Qed.


Theorem optmald :
  forall a s, val a s = val (optmal a) s.
Proof.
  induction a; intros ?; simpl; auto.
  destruct (aqb a1 a2) eqn:H;
    rewrite IHa1, IHa2; auto;
      clear IHa1 IHa2.
  simpl; apply f_equal, aeq_val; auto.
Qed.
于 2021-04-04T15:20:06.037 回答
0

首先，unfold val最好依靠simplafterinduction来简化事情，而不是 ，因为这通常会导致目标更容易阅读。

Theorem optmald :
  forall a s, val a s = val (optmal a) s.
Proof.
intros. induction a; simpl.
* reflexivity.
* reflexivity.
*

现在目标看起来像

val a1 s + val a2 s =
val (if aqb a1 a2 then ADup (optmal a1) else APlus (optmal a1) (optmal a2)) s

当目标中有一个if（或一个match）时，一个通常好的步骤是向destruct审查员：

destruct (aqb a1 a2) eqn:Ea.
于 2021-04-03T15:46:03.797 回答