■

一日寝てた。

昨日のCoq

別に間違っておらんかった。間違ってたのは、omegaの使い方のようだ。
詰るところ使い方がわからん。

• 数値定数、加算(+とS)、減算(-とpred)、 定数の積算(これがプレスバーガー算術である条件です)、
• 等式(=と<>)および不等式(<=)、
• 論理演算子∧, ∨, ~, →

つまり、数式しかあかんのか。boolがあったり、独自演算があるともうあかんと。

昨日出来なかったのは、単に、generalize dependent のつかいどころが分かってなかったためのようだ。少し長くなるともう分からん。証明も仮定も。

Reserved Notation "e '||' n" (at level 50, left associativity).

Inductive bevalR : bexp -> bool -> Prop :=
  | E_BTrue : BTrue || true
  | E_BFalse : BFalse || false
  | E_BEq : forall (a1 a2: aexp), (BEq a1 a2) ||  beq_nat (aeval a1) (aeval a2)
  | E_BLe : forall (a1 a2 : aexp), (BLe a1 a2) || ble_nat (aeval a1) (aeval a2)
  | E_BNot : forall (be : bexp) (b : bool) , 
     (be || b) -> (BNot be) || (negb b)
  | E_BAnd : forall (be1 be2 : bexp) (b1 b2: bool), 
     be1 || b1 -> be2 || b2 -> 
     (BAnd be1 be2) || (andb b1 b2)
 where "e '||' b" := (bevalR e b) : type_scope.

Theorem beval_iff_bevalR : forall (be : bexp) (b : bool),
  (be || b) <-> beval be = b.
Proof.
  intros.
  split.
  Case "->".
    intros H. induction H.
      SCase "E_BTrue". reflexivity. 
      SCase "E_BFalse". reflexivity.
      SCase "E_BEq". reflexivity.
      SCase "E_BLe". reflexivity.
      SCase "E_BNot". subst.  reflexivity.
      SCase "E_BAnd". subst.  reflexivity.
  Case "<-".
    intros. generalize dependent b.  induction be.
      SCase "BTrue". simpl. intros. subst. apply E_BTrue. 
      SCase "BFalse". simpl. intros. subst. apply E_BFalse. 
      SCase "BEq". intros. subst. apply E_BEq.
      SCase "BLe". intros. subst. apply E_BLe. 
      SCase "BNot". intros. subst. simpl. apply E_BNot. apply IHbe. reflexivity.
      SCase "BAnd". intros. subst. simpl. apply E_BAnd.
        apply IHbe1. reflexivity. apply IHbe2. reflexivity.
  Qed.

これをどうまとめればいいのか。

.単純にまとめると

  Theorem beval_iff_bevalR_short : forall be b, bevalR be b <-> beval be = b.
  Proof.
    split.
    Case "->".
      intros H; induction H; simpl; subst; reflexivity.
    Case "<-".
    intros. generalize dependent b.
    induction be;  simpl; intros; subst; constructor;
      try (apply IHbe; reflexivity);
      try (apply IHbe1; reflexivity); try (apply IHbe2; reflexivity).
  Qed.

って演算子って bevalでもaevalでも使えるの？よくわかんねーな。