The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

Many thanks, Gaëtan!  Yes, this works.

May I trouble you (and/or others) with one further question?  When I scale this up to the full Imp language, it seems to get me almost everything I want, but I am still puzzled by why I can't omit the parentheses on the very last line below.  I've tried tweaking various precedence levels, but have not found the right combination...

   - B

From Coq Require Import Strings.String. Import String.
From Coq Require Import Bool.Bool.
From Coq Require Import Init.Nat.
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat. Import Nat.
From Coq Require Import Lia.
From Coq Require Import Lists.List. Import ListNotations.
From PLF Require Import Maps.

Declare Custom Entry com.
Declare Custom Entry com_aux.
Declare Scope com_scope.
Open Scope com_scope.

Definition state := total_map nat.

Inductive aexp : Type :=
  | ANum (n : nat)
  | AId (x : string)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).

Definition W : string := "W".
Definition X : string := "X".
Definition Y : string := "Y".
Definition Z : string := "Z".

Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BNeq (a1 a2 : aexp)
  | BLe (a1 a2 : aexp)
  | BGt (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

Coercion AId : string >-> aexp.
Coercion ANum : nat >-> aexp.

Notation "<{ e }>" := e (e custom com_aux) : com_scope.
Notation "e" := e (in custom com_aux at level 0, e custom com) : com_scope.

Notation "( x )" := x (in custom com, x at level 98) : com_scope.
Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope.
Notation "f x .. y" := (.. (f x) .. y)
                  (in custom com at level 0, only parsing,
                  f constr at level 0, x constr at level 9,
                  y constr at level 9) : com_scope.

Notation "x + y"   := (APlus x y) (in custom com at level 50, left associativity).
Notation "x - y"   := (AMinus x y) (in custom com at level 50, left associativity).
Notation "x * y"   := (AMult x y) (in custom com at level 40, left associativity).
Notation "'true'"  := true (at level 1).
Notation "'true'"  := BTrue (in custom com at level 0).
Notation "'false'" := false (at level 1).
Notation "'false'" := BFalse (in custom com at level 0).
Notation "x <= y"  := (BLe x y) (in custom com at level 70, no associativity).
Notation "x > y"   := (BGt x y) (in custom com at level 70, no associativity).
Notation "x = y"   := (BEq x y) (in custom com at level 70, no associativity).
Notation "x <> y"  := (BNeq x y) (in custom com at level 70, no associativity).
Notation "x && y"  := (BAnd x y) (in custom com at level 80, left associativity).
Notation "'~' b"   := (BNot b) (in custom com at level 75, right associativity).

Locate "=".
Check <{ X + Y }>.
Check <{ X + Y = 0 }>.
Check <{ ~ (Y = X) }>.
Check <{ X + Y }>.
Check <{ ~ (X + Y = Y) && Z = W }>.

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

Notation "'skip'"  :=
         CSkip (in custom com at level 0) : com_scope.
Notation "x := y"  :=
         (CAsgn x y)
            (in custom com at level 0, x constr at level 0,
             y at level 85, no associativity) : com_scope.
Notation "x ; y" :=
         (CSeq x y)
           (in custom com at level 90,
            right associativity) : com_scope.
Notation "'if' x 'then' y 'else' z 'end'" :=
         (CIf x y z)
           (in custom com at level 89, x at level 98,
            y at level 98, z at level 98) : com_scope.
Notation "'while' x 'do' y 'end'" :=
         (CWhile x y)
           (in custom com at level 89, x at level 98,
            y at level 98) : com_scope.

Check <{ skip }>.
Check <{ (skip ; skip) ; skip }>.
Check <{ 1 + 2 }>.
Check <{ 2 = 1 }>.
Check <{ Z := X }>.
Check <{ Z := X + 3 }>.
Definition func (c : com) : com := <{ c ; skip }>.
Check <{ skip; func <{ skip }> }>.
Definition func2 (c1 c2 : com) : com := <{ c1 ; c2 }>.
Check <{ skip ; func2 <{skip}> <{skip}> }>.
Check <{ true && ~(false && true) }>.
Check <{ if true then skip else skip end }>.
Check <{ if true && true then skip; skip else skip; X:=X+1 end }>.
Check <{ while Z <> 0 do Y := Y * Z; Z := Z - 1 end }>.

Fixpoint aeval (st : state) (* <--- NEW *)
               (a : aexp) : nat :=
  match a with
  | ANum n => n
  | AId x => st x                                (* <--- NEW *)
  | <{a1 + a2}> => (aeval st a1) + (aeval st a2)
  | <{a1 - a2}> => (aeval st a1) - (aeval st a2)
  | <{a1 * a2}> => (aeval st a1) * (aeval st a2)
  end.

Fixpoint beval (st : state) (* <--- NEW *)
               (b : bexp) : bool :=
  match b with
  | <{true}>      => true
  | <{false}>     => false
  | <{a1 = a2}>   => (aeval st a1) =? (aeval st a2)
  | <{a1 <> a2}>  => negb ((aeval st a1) =? (aeval st a2))
  | <{a1 <= a2}>  => (aeval st a1) <=? (aeval st a2)
  | <{a1 > a2}>   => negb ((aeval st a1) <=? (aeval st a2))
  | <{~ b1}>      => negb (beval st b1)
  | <{b1 && b2}>  => andb (beval st b1) (beval st b2)
  end.

Definition Assertion := state -> Prop.

Definition Assert_of_bexp (b : bexp) : Assertion := fun st => beval st b = true.

Notation "{ P } e { Q }" :=
  ((Assert_of_bexp P), e, (Assert_of_bexp Q))
    (in custom com_aux,
     e custom com,
     P custom com,
     Q custom com) : com_scope.

Check (<{ X > 0 }>).
Check (<{ X := 0 }>).
Check (<{ { X > 0 } (X := 0) { true } }>).
Check (<{ { X > 0 } X := 0 { true } }>).