「SF-LC」12 Imp

零式的天空

发布于 2022-03-14 14:43:06

1.7K0

发布于 2022-03-14 14:43:06

文章被收录于专栏：零域Blog

Z ::= X;;
Y ::= 1;;
WHILE ~(Z = 0) DO
  Y ::= Y * Z;;
  Z ::= Z - 1
END

A weird convention through out all IMP is:

a-: arith
b-: bool
c-: command

Arithmetic and Boolean Expression

Abstract Syntax

a ::=
    | nat
    | a + a
    | a - a
    | a * a
b ::= 
    | true
    | false
    | a = a
    | a ≤ a
    | ¬b
    | b && b

Inductive aexp : Type :=
  | ANum (n : nat)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).
Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BLe (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

Evaluation

TODO: is this considered as “denotational semantics”?

Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n ⇒ n
  | APlus a1 a2 ⇒ (aeval a1) + (aeval a2)
  | AMinus a1 a2 ⇒ (aeval a1) - (aeval a2)
  | AMult a1 a2 ⇒ (aeval a1) * (aeval a2)
  end.
Fixpoint beval (b : bexp) : bool :=
  match b with
  | BTrue ⇒ true
  | BFalse ⇒ false
  | BEq a1 a2 ⇒ (aeval a1) =? (aeval a2)
  | BLe a1 a2 ⇒ (aeval a1) <=? (aeval a2)
  | BNot b1 ⇒ negb (beval b1)
  | BAnd b1 b2 ⇒ andb (beval b1) (beval b2)
  end.

Supposed we have a Fixpoint optimize_0plus (a:aexp) : aexp

Theorem optimize_0plus_sound: ∀a,
  aeval (optimize_0plus a) = aeval a.

During the proof, many cases of destruct aexp are similar! Recursive cases such as APlus, AMinus, AMult all require duplicated IH application.

From Coq Intensive: when we simpl on APlus case. it’s not “simplified” but give us a pattern matching. That’s a hint that we need to furthur case analysis by destruct n as 0 case or _ case.

Coq Automation

Tacticals

“higher-order tactics”.

`try T` and `;` tacticals

if T fail, try T successfully does nothing at all T;T' : performs T' on each subgoal generated by T.

Super blindly but useful: (only leave the “interesting” one.)

induction a;
    (* Most cases follow directly by the IH... *)
    try (simpl; rewrite IHa1; rewrite IHa2; reflexivity).
    (* ... or are immediate by definition *)
    try reflexivity.

. is the atomic ; cannot be stepped into…

`T; [T1 | T2 | ... | Tn]` tacticals

general form or ; T;T' is shorthand for: T; [T' | T' | ... | T'].

`repeat` tacticals

Theorem In10 : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
  repeat (try (left; reflexivity); right). Qed.

stop when it fails
always succeeds, then loop forever! e.g. repeat simpl

This does not affect Coq’s logical consistency, construction process diverges means we have failed to construct a proof, not that we have constructed a wrong one.

Defining New Tactic Notations

Tactic Notation: syntax extension for tactics (good for simple macros)

Tactic Notation "simpl_and_try" tactic(c) :=
  simpl; try c.

Ltac: scripting language for tactics (good for more sophisticated proof engineering)
OCaml tactic scripting API (for wizards)

The `omega` Tactic

Presburger arithmetic

arith, equality, ordering, logic connectives
O(doubly expontential)

A Few More Handy Tactics

clear H
subst x, subst
rename ... into ... (change auto-generated name that we don’t like…)

the below three are very useful in Coq Automation (w/ try T; T')

assumption

contradiction

constructorapply

            Problem: might have multiple constructors applicable but some fail)

Evaluation as a Relation

Defined as Binary relation on aexp × nat. Exactly Big Step / Structural Operational Semantics.

More flexible than Fixpoint (computation, or Denotational). …Since we can operate on Inductive as data I guess? …and we can also induction on the relation. …and when things getting more and more “un-computable” (see below).

译注：求值关系不满足对称性，因为它是有方向的。

Inductive aevalR : aexp → nat → Prop :=
  | E_ANum n :
      aevalR (ANum n) n
  | E_APlus (e1 e2: aexp) (n1 n2: nat) :
      aevalR e1 n1 →
      aevalR e2 n2 →
      aevalR (APlus e1 e2) (n1 + n2)
  | E_AMinus (e1 e2: aexp) (n1 n2: nat) :
      aevalR e1 n1 →
      aevalR e2 n2 →
      aevalR (AMinus e1 e2) (n1 - n2)
  | E_AMult (e1 e2: aexp) (n1 n2: nat) :
      aevalR e1 n1 →
      aevalR e2 n2 →
      aevalR (AMult e1 e2) (n1 * n2).

Noticed now we now define inductive in a mixed style: some arg is before : (named), some are after : (anonymous).

We could do this as well

| E_APlus (e1 e2: aexp) (n1 n2: nat)
     (H1 : aevalR e1 n1)
     (H2 : aevalR e2 n2) :
     aevalR (APlus e1 e2) (n1 + n2)

Reserved Notation allow us using the notation during the definition!

Reserved Notation "e '\\' n" (at level 90, left associativity).

Inductive aevalR : aexp → nat → Prop :=
  | E_ANum (n : nat) :
      (ANum n) \\ n
  | E_APlus (e1 e2 : aexp) (n1 n2 : nat) :
      (e1 \\ n1) → 
      (e2 \\ n2) → 
      (APlus e1 e2) \\ (n1 + n2)
  | E_AMinus (e1 e2 : aexp) (n1 n2 : nat) :
      (e1 \\ n1) → 
      (e2 \\ n2) → 
      (AMinus e1 e2) \\ (n1 - n2)
  | E_AMult (e1 e2 : aexp) (n1 n2 : nat) :
      (e1 \\ n1) → 
      (e2 \\ n2) → 
      (AMult e1 e2) \\ (n1 * n2)

  where "e '\\' n" := (aevalR e n) : type_scope.

I hated this infix \\ notation…it tries to mimic ⇓ (double down arrow).

                           e1 \\ n1
                           e2 \\ n2
                     -------------------- (E_APlus)
                     APlus e1 e2 \\ n1+n2

is actually:

                           e1 ⇓ n1
                           e2 ⇓ n2
                     -------------------- (E_APlus)
                     APlus e1 e2 ⇓ n1+n2

Coq Intensive: If you have two variables above the line. Think about if you need generalize dependent.

Computational vs. Relational Definitions INTERESTING

In some cases, relational definition are much better than computational (a.k.a. functional).

for situations, where thing beingdefined is not easy to express as a function (or not a function at all)

case 1 - safe division

Inductive aexp : Type :=
| ADiv (a1 a2 : aexp). (* <--- NEW *)

functional: how to return ADiv (ANum 5) (ANum 0)? probably has to be option (Coq is total!)
relational: (a1 \\ n1) → (a2 \\ n2) → (n2 > 0) → (mult n2 n3 = n1) → (ADiv a1 a2) \\ n3.
- we can add a constraint (n2 > 0).

case 2 - non-determinism

Inductive aexp : Type :=
| AAny (* <--- NEW *)

functional: not a deterministic function…
relational: E_Any (n : nat) : AAny \\ n … just say it’s the case.

Nonetheless, functional definition is good at:

by definition deterministic (need proof in relational case)
take advantage of Coq’s computation engine.
function can be directly “extracted” from Gallina to OCaml/Haskell

In large Coq developments:

given both styles
a lemma stating they coincise (等价)

Expressions with Variables

State (Environment) 环境

A machine state (or just state) represents the current values of all variables at some point in the execution of a program.

Definition state := total_map nat.

Syntax

Inductive aexp : Type :=
  | AId (x : string) (* <--- NEW *)

Notations & Coercisons — “meta-programming” and AST quasi-quotation

Quasi-quotation

OCaml PPX & AST quasi-quotation

quasi-quotation enables one to introduce symbols that stand for a linguistic expression in a given instance and are used as that linguistic expression in a different instance.

e.g. in above OCaml example, you wrote %expr 2 + 2 and you get [%expr [%e 2] + [%e 2]].

Coq’s Notation Scope + Coercision == built-in Quasi-quotation

(** Coercision for constructors **)
Coercion AId : string >-> aexp.
Coercion ANum : nat >-> aexp.

(** Coercision for functions **)
Definition bool_to_bexp (b : bool) : bexp := if b then BTrue else BFalse.
Coercion bool_to_bexp : bool >-> bexp.

(** Scoped Notation **)
Bind Scope imp_scope with aexp.
Bind Scope imp_scope with bexp.

(** the Extension Point token **)
Delimit Scope imp_scope with imp.

(** now we can write... **)
Definition example_aexp := (3 + (X * 2))%imp : aexp.
Definition example_aexp : aexp := (3 + (X * 2))%imp. 
Definition example_aexp := (3 + (X * 2))%imp.    (* can be inferred *)

Evaluation w/ State (Environment)

Noticed that the st has to be threaded all the way…

Fixpoint aeval (st : state) (a : aexp) : nat :=
  match a with
  | AId x ⇒ st x (* <--- NEW *)              (** lookup the environment **)
  ...

Fixpoint beval (st : state) (b : bexp) : bool := ...

Compute (aeval (X !-> 5) (3 + (X * 2))%imp). (** ===> 13 : nat **)

Commands (Statement)

c ::= SKIP | x ::= a | c ;; c | TEST b THEN c ELSE c FI | WHILE b DO c END

we use TEST to avoid conflicting with the if and IF notations from the standard library.

Inductive com : Type :=
  | CSkip
  | CAss (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).

notation magics:

Bind Scope imp_scope with com.
Notation "'SKIP'" := CSkip : imp_scope.
Notation "x '::=' a" := (CAss x a) (at level 60) : imp_scope.
Notation "c1 ;; c2" := (CSeq c1 c2) (at level 80, right associativity) : imp_scope.
Notation "'WHILE' b 'DO' c 'END'" := (CWhile b c) (at level 80, right associativity) : imp_scope.
Notation "'TEST' c1 'THEN' c2 'ELSE' c3 'FI'" := (CIf c1 c2 c3) (at level 80, right associativity) : imp_scope.

Unset Notations

Unset Printing Notations.  (** e1 + e2 -> APlus e1 e2 **)
Set Printing Coercions.    (** n -> (ANum n) **)
Set Printing All.

The `Locate` command

Locate "&&".

(** give you two, [Print "&&"] only give you the default one **)
Notation
"x && y" := andb x y : bool_scope (default interpretation)
"x && y" := BAnd x y : imp_scope

Evaluating Commands

Noticed that to use quasi-quotation in pattern matching, we need

Open Scope imp_scope.
...
  | x ::= a1 =>     (**  CAss x a1  **)
  | c1 ;; c2 =>     (**  CSeq c1 c1 **)
...
Close Scope imp_scope.

An infinite loop (the %imp scope is inferred)

Definition loop : com :=
  WHILE true DO
    SKIP
  END.

The fact that WHILE loops don’t necessarily terminate makes defining an evaluation function tricky…

Evaluation as function (FAIL)

In OCaml/Haskell, we simply recurse, but In Coq

| WHILE b DO c END => if (beval st b)
                      then ceval_fun st (c ;; WHILE b DO c END)
                      else st
(** Cannot guess decreasing argument of fix **)

Well, if Coq allowed (potentially) non-terminating, the logic would be inconsistent:

Fixpoint loop_false (n : nat) : False := loop_false n.   (** False is proved! **)

Step-Indexed Evaluator (SUCC)

Chapter ImpCEvalFun provide some workarounds to make functional evalution works:

step-indexed evaluator, i.e. limit the recursion depth. (think about Depth-Limited Search).
return option to tell if it’s a normal or abnormal termination.
use LETOPT...IN... to reduce the “optional unwrapping” (basicaly Monadic binding >>=!)
- this approach of let-binding became so popular in ML family.

Evaluation as Relation (SUCC)

Again, we are using some fancy notation st=[c]=>st' to mimic ⇓: In both PLT and TaPL, we are almost exclusively use Small-Step, but in PLC, Big-Step were used:

                      beval st b1 = true
                       st =[ c1 ]=> st'
            ---------------------------------------  (E_IfTrue)
            st =[ TEST b1 THEN c1 ELSE c2 FI ]=> st'

is really:

                        H; b1 ⇓ true
                        H; c1 ⇓ H'
              ----------------------------------  (E_IfTrue)
              H; TEST b1 THEN c1 ELSE c2 FI ⇓ H'

Reserved Notation "st '=[' c ']⇒' st'" (at level 40).
Inductive ceval : com → state → state → Prop :=
...
| E_Seq : ∀c1 c2 st st' st'',
    st =[ c1 ]⇒ st' →
    st' =[ c2 ]⇒ st'' →
    st =[ c1 ;; c2 ]⇒ st''
| E_IfTrue : ∀st st' b c1 c2,
      beval st b = true →
      st =[ c1 ]⇒ st' →
      st =[ TEST b THEN c1 ELSE c2 FI ]⇒ st'
...
  where "st =[ c ]⇒ st'" := (ceval c st st').

By definition evaluation as relation (in Type level), we need to construct proofs (terms) to define example.

…noticed that in the definition of relaiton ceval, we actually use the computational aevel, beval.. …noticed that we are using explicit ∀ style rather than constructor argument style (for IDK reason). They are the same!

Determinism of Evaluation

Changing from a computational to a relational definition of evaluation is a good move because it frees us from the artificial requirement that evaluation should be a total function 求值不再必须是全函数 But it also raises a question: Is the second definition of evaluation really a partial function? 这个定义真的是偏函数吗？（这里的重点在于偏函数要求 right-unique 即 deterministic）

we can prove:

Theorem ceval_deterministic: ∀c st st1 st2,
     st =[ c ]⇒ st1 →
     st =[ c ]⇒ st2 →
     st1 = st2.
Proof. ...

Reasoning About Imp Programs

Case `plus2_spec`

Theorem plus2_spec : ∀st n st',
  st X = n →
  st =[ plus2 ]⇒ st' →
  st' X = n + 2.
Proof.
  intros st n st' HX Heval.

this looks much better as inference rules:

    H(x) = n
    H; x := x + 2 ⇓ H'
  --------------------- (plus2_spec)
    H'(x) = n + 2

By inversion on the Big Step eval relation, we can expand one step of ceval (对 derivation tree 的 expanding 过程其实就是展开我们所需的计算步骤的过程)

  st : string -> nat
  =================================
  (X !-> st X + 2; st) X = st X + 2

In inference rule:

  H : string → nat
  ================================
  (x ↦ H(x) + 2); H)(x) = H(x) + 2

Case `no_whiles_terminating`

Theorem no_whilesR_terminating_fail:
   forall c, no_whilesR c -> forall st, exists st', st =[ c ]=> st'.
Proof.
  intros.
  induction H; simpl in *. 
  - admit.
  - admit.
  - (* E_Seq *)

If we intros st before induction c, the IH would be for particular st and too specific for E_Seq (It’s actually okay for TEST since both branch derive from the same st)

IHno_whilesR1 : exists st' : state, st =[ c1 ]=> st'
IHno_whilesR2 : exists st' : state, st =[ c2 ]=> st'
============================
exists st' : state, st =[ c1;; c2 ]=> st'

So we’d love to

generalize dependent st.
induction H...
- specialize (IHno_whilesR1 st).  destruct IHno_whilesR1 as [st' Hc1].
  specialize (IHno_whilesR2 st'). destruct IHno_whilesR2 as [st'' Hc2].  (* specialize [IH2] with the existential of [IH1] **)
  exists st''.
  apply E_Seq with (st'); assumption.

Additional Exerciese

Stack Compiler

Things that evaluate arithmetic expressions using stack:

Old HP Calculators
Forth, Postscript
Java Virtual Machine

infix:
      (2*3)+(3*(4-2))

postfix:
      2 3 * 3 4 2 - * +

stack:
      [ ]           |    2 3 * 3 4 2 - * +
      [2]           |    3 * 3 4 2 - * +
      [3, 2]        |    * 3 4 2 - * +
      [6]           |    3 4 2 - * +
      [3, 6]        |    4 2 - * +
      [4, 3, 6]     |    2 - * +
      [2, 4, 3, 6]  |    - * +
      [2, 3, 6]     |    * +
      [6, 6]        |    +
      [12]          |

Goal: compiler translates aexp into stack machine instructions.

Inductive sinstr : Type :=
| SPush (n : nat)
| SLoad (x : string)   (* load from store (heap) *)
| SPlus
| SMinus
| SMult.

Correct Proof

Theorem s_compile_correct : forall (st : state) (e : aexp),
  s_execute st [] (s_compile e) = [ aeval st e ].

To prove this, we need a stronger induction hypothesis (i.e. more general), so we state:

Theorem s_execute_theorem : forall (st : state) (e : aexp) (stack : list nat) (prog : list sinstr),
  s_execute st stack (s_compile e ++ prog) = s_execute st ((aeval st e) :: stack) prog.

and go through!

IMP `Break/Continue`

Inductive result : Type :=
  | SContinue
  | SBreak.

The idea is that we can add a signal to notify the loop!

Fun to go through!

Slide Q & A

st =[c1;;c2] => st'

there would be intermediate thing after inversion so… we need determinism to prove this!
- (It won’t be even true in undetermincy)
the WHILE one (would diverge)
- true…how to prove?
- induction on derivation…!
  - show contradiction for all cases
to prove ¬(∃st', ...), we intro the existentials and prove the False.

`Auto`

auto includes try

Proof with auto.
Set Intro Auto

本文参与腾讯云自媒体同步曝光计划，分享自作者个人站点/博客。

原始发表：2021-03-28，如有侵权请联系 cloudcommunity@tencent.com 删除

编程算法

面向对象编程

本文分享自作者个人站点/博客前往查看

如有侵权，请联系 cloudcommunity@tencent.com 删除。

本文参与腾讯云自媒体同步曝光计划，欢迎热爱写作的你一起参与！

编程算法

面向对象编程

登录后参与评论

0 条评论

热度

「SF-LC」12 Imp

「SF-LC」12 Imp

Arithmetic and Boolean Expression

Abstract Syntax

Evaluation

Coq Automation

Tacticals

try T and ; tacticals

T; [T1 | T2 | ... | Tn] tacticals

repeat tacticals

Defining New Tactic Notations

The omega Tactic

A Few More Handy Tactics

Evaluation as a Relation

Computational vs. Relational Definitions INTERESTING

case 1 - safe division

case 2 - non-determinism

Expressions with Variables

State (Environment) 环境

Syntax

Notations & Coercisons — “meta-programming” and AST quasi-quotation

Quasi-quotation

Coq’s Notation Scope + Coercision == built-in Quasi-quotation

Evaluation w/ State (Environment)

Commands (Statement)

Unset Notations

The Locate command

Evaluating Commands

Evaluation as function (FAIL)

Step-Indexed Evaluator (SUCC)

Evaluation as Relation (SUCC)

Determinism of Evaluation

Reasoning About Imp Programs

Case plus2_spec

Case no_whiles_terminating

Additional Exerciese

Stack Compiler

Correct Proof

IMP Break/Continue

Slide Q & A

Auto

社区

活动

资源

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

`try T` and `;` tacticals

`T; [T1 | T2 | ... | Tn]` tacticals

`repeat` tacticals

The `omega` Tactic

The `Locate` command

Case `plus2_spec`

Case `no_whiles_terminating`

IMP `Break/Continue`

`Auto`