imp.v

Require Export SfLib.
Require Import Strings.String.
Require Import ZArith.

Module AExp.

Inductive aexp : Type :=
  | ANum : nat -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

Inductive bexp : Type :=
  | BTrue : bexp
  | BFalse : bexp
  | BEq : aexp -> aexp -> bexp
  | BLe : aexp -> aexp -> bexp
  | BNot : bexp -> bexp
  | BAnd : bexp -> bexp -> bexp.

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.

Example test_aeval1: aeval (APlus (ANum 2) (ANum 2)) = 4.
Proof. reflexivity. Qed.

Fixpoint beval (b : bexp) : bool :=
  match b with
  | BTrue => true
  | BFalse => false
  | BEq a1 a2 => beq_nat (aeval a1) (aeval a2)
  | BLe a1 a2 => ble_nat (aeval a1) (aeval a2)
  | BNot b1 => negb (beval b1)
  | BAnd b1 b2 => andb (beval b1) (beval b2)
  end.

Fixpoint optimize_0plus (a : aexp) : aexp :=
  match a with
  | ANum n => ANum n
  | APlus (ANum 0) e2 => optimize_0plus e2
  | APlus e1 e2 => APlus (optimize_0plus e1) (optimize_0plus e2)
  | AMinus e1 e2 => AMinus (optimize_0plus e1) (optimize_0plus e2)
  | AMult e1 e2 => AMult (optimize_0plus e1) (optimize_0plus e2)
  end.

Tactic Notation "aexp_cases" tactic(induction_tactic) ident(case_level) :=
  induction_tactic;
    [ Case_aux case_level "ANum"
    | Case_aux case_level "APlus"
    | Case_aux case_level "AMinus"
    | Case_aux case_level "AMult"
    ].
    
Theorem optimize_0plus_sound : forall a,
  aeval (optimize_0plus a) = aeval a.
Proof.
  intros a.
  aexp_cases (induction a) Case;
    try reflexivity;
    try (simpl;
         rewrite IHa1;
         rewrite IHa2;
         reflexivity).
  Case "APlus".
    destruct a1;
      try (simpl in IHa1;
           simpl;
           rewrite IHa1;
           rewrite IHa2;
           reflexivity).
    SCase "a1 = ANum n".
      destruct n as [ | n'];
        simpl;
        rewrite IHa2;
        reflexivity.
Qed.

Theorem ev100 : ev 100.
Proof.
  repeat (apply ev_SS).
  apply ev_0.
Qed.

Theorem silly1 : forall ae, aeval ae = aeval ae.
Proof.
  try reflexivity.
Qed.

Theorem silly2 : forall P : Prop, P -> P.
Proof.
  intros P HP.
  try reflexivity.
  apply HP.
Qed.

Lemma foo : forall n, ble_nat 0 n = true.
Proof.
  intros.
  destruct n; reflexivity.
Qed.

Print bexp.

Fixpoint optimize_0plus_b (b : bexp) : bexp :=
  match b with
  | BTrue => BTrue
  | BFalse => BFalse
  | BEq a1 a2 => BEq (optimize_0plus a1) (optimize_0plus a2)
  | BLe a1 a2 => BLe (optimize_0plus a1) (optimize_0plus a2)
  | BNot b => BNot (optimize_0plus_b b)
  | BAnd b1 b2 => BAnd (optimize_0plus_b b1) (optimize_0plus_b b2)
  end.                       

Tactic Notation "bexp_cases" tactic(induction_tactic) ident(case_level) :=
  induction_tactic;
    [ Case_aux case_level "BTrue"
    | Case_aux case_level "BFalse"
    | Case_aux case_level "BEq"
    | Case_aux case_level "BLe"
    | Case_aux case_level "BNot"
    | Case_aux case_level "BAnd"
    ].

Theorem optimize_0plus_b_sound : forall b : bexp,
  beval (optimize_0plus_b b) = beval b.                                 
Proof.
  induction b as [ | | | | b IHb1 | b1 IHb1 b2 IHb2];
    try reflexivity;
    try (simpl;
         repeat (rewrite optimize_0plus_sound);
         reflexivity);
    simpl;
    rewrite IHb1;
    try rewrite IHb2;
    reflexivity.
Qed.


Example silly_presburger_example : forall m n o p,
  m + n <= n + o /\ o + 3 = p + 2 ->
  m < p.
Proof.
  intros.
  omega.
Qed.

Print silly_presburger_example.

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

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum : forall (n : nat), (ANum n) --> n
  | E_APlus : forall (e1 e2 : aexp) (n1 n2 : nat),
      (e1 --> n1) -> (e2 --> n2) -> (APlus e1 e2) --> (n1 + n2)
  | E_AMinus : forall (e1 e2 : aexp) (n1 n2 : nat),
      (e1 --> n1) -> (e2 --> n2) -> (AMinus e1 e2) --> (n1 - n2)
  | E_AMult : forall (e1 e2 : aexp) (n1 n2 : nat),
      (e1 --> n1) -> (e2 --> n2) -> (AMult e1 e2) --> (n1 * n2)
  where "e '-->' n" := (aevalR e n) : type_scope.

Tactic Notation "aevalR_cases" tactic(induction_tactic)
                               ident(case_level) :=
  induction_tactic;
    [ Case_aux case_level "E_ANum"
    | Case_aux case_level "E_APlus"
    | Case_aux case_level "E_AMinus"
    | Case_aux case_level "E_AMult"
    ].
    
Theorem aeval_iff_aevalR : forall a n,
  (a --> n) <-> aeval a = n.
Proof.
  split.
  Case "->".
    intros A.
    aevalR_cases (induction A) SCase;
      subst;
      reflexivity.
  Case "<-".
    generalize dependent n.
    aexp_cases (induction a) SCase;
      intros m eq;
      simpl in eq;
      subst;
      constructor;
      try apply IHa1;
      try apply IHa2;
      reflexivity.
Qed.

Print bexp.
    
Reserved Notation "e '~>' b" (at level 50, left associativity).

Inductive bevalR : bexp -> bool -> Prop :=
  | E_BTrue : BTrue ~> true
  | E_BFalse : BFalse ~> false
  | E_BEq : forall (e1 e2 : aexp) (n1 n2 : nat),
      (e1 --> n1) -> (e2 --> n2) -> (BEq e1 e2 ~> beq_nat n1 n2)
  | E_BLe : forall (e1 e2 : aexp) (n1 n2 : nat),
      (e1 --> n1) -> (e2 --> n2) -> (BLe e1 e2 ~> ble_nat n1 n2)
  | E_Not : forall (e1 : bexp) (b1 : bool),
      (e1 ~> b1) -> (BNot e1 ~> negb b1)                              
  | E_BAnd : forall (e1 e2 : bexp) (b1 b2 : bool),
      (e1 ~> b1) -> (e2 ~> b2) -> (BAnd e1 e2 ~> andb b1 b2)
  where "e '~>' b" := (bevalR e b) : type_scope.


Theorem beval_iff_bevalR : forall bexpr b,
  (bexpr ~> b) <-> beval bexpr = b.
Proof.
  split.
  Case "->".
    intros B.
    induction B;
      try reflexivity;
      try (simpl;
           apply aeval_iff_aevalR in H;
           apply aeval_iff_aevalR in H0;
           subst;
           reflexivity);
      simpl;
      subst;
      reflexivity.
  Case "<-".
    generalize dependent b.
    bexp_cases (induction bexpr) SCase;
      intros b eq;
      subst;
      simpl;
      try (constructor;
           apply aeval_iff_aevalR;
           reflexivity);
      try (constructor;
           try apply IHbexpr;
           try apply IHbexpr1;
           try apply IHbexpr2;
           reflexivity).
Qed.

Print beval_iff_bevalR.

Module LanguageL.

Inductive simple_binop_symbol : Set :=
  | Plus
  | Minus
  | Prod
  | Eq
  | Neq
  | Le
  | Lt
  | Ge
  | Gt.

Inductive divmod_binop_symbol : Set :=
  | Div
  | Mod.

Inductive discon_binop_symbol : Set :=
  | Disj
  | Conj.

Inductive expr : Set :=
  | Const : nat -> expr
  | Var : string -> expr
  | BinOp : simple_binop_symbol -> expr -> expr -> expr
  | BinDM : divmod_binop_symbol -> expr -> expr -> expr
  | BinDC : discon_binop_symbol -> expr -> expr -> expr.

Check (BinOp Plus (Var "x") (Const 1)).

Definition z_of_bool (b : bool) : Z.t :=
  match b with
  | true => Z.one
  | false => Z.zero
  end.

Definition simple_binop (sym : simple_binop_symbol) : Z.t -> Z.t -> Z.t :=
  match sym with
  | Plus => Z.add
  | Minus => Z.sub
  | Prod => Z.mul
  | Eq => fun x y => z_of_bool (Z.eqb x y)
  | Neq => fun x y => z_of_bool (negb (Z.eqb x y))
  | Le => fun x y => z_of_bool (Z.leb x y)
  | Lt => fun x y => z_of_bool (Z.ltb x y)
  | Ge => fun x y => z_of_bool (Z.geb x y)
  | Gt => fun x y => z_of_bool (Z.gtb x y)
  end.

Eval compute in simple_binop Plus Z.one Z.two.

Inductive eval_rel : expr -> Z.t -> Prop :=
  | EvalConst : forall n : nat, eval_rel (Const n) (Z.of_nat n)
  | EvalBinOp : forall (sym : simple_binop_symbol) (e1 e2 : expr) (z1 z2 : Z.t),
      (eval_rel e1 z1) ->
      (eval_rel e2 z2) ->
      eval_rel (BinOp sym e1 e2) (simple_binop sym z1 z2).

Example simple_binop_test1 : eval_rel (BinOp Plus (Const 1) (Const 2)) (Z.of_nat 3).
Proof.
  apply EvalBinOp with
      (sym := Plus) (e1 := Const 1) (e2 := Const 2) (z1 := Z.one) (z2 := Z.two);
    constructor.
Qed.

End LanguageL.

Inductive id : Type :=
  Id : nat -> id.

Theorem eq_id_dec : forall id1 id2 : id, {id1 = id2} + {id1 <> id2}.
Proof.
  intros id1 id2.
  destruct id1 as [n1].
  destruct id2 as [n2].
  destruct (eq_nat_dec n1 n2) as [Heq | Hneq].
    subst.
    left.
    reflexivity.
  right.
  intros contra.
  inversion contra.
  apply Hneq in H0.
  contradiction.
Qed.

Lemma eq_id : forall (T : Type) x (p q : T),
  (if eq_id_dec x x then p else q) = p.
Proof.
  intros T x p q.
  destruct (eq_id_dec x x).
    reflexivity.
  apply ex_falso_quodlibet.
  apply n.
  reflexivity.
Qed.

Lemma neq_id : forall (T : Type) x y (p q : T), x <> y ->
  (if eq_id_dec x y then p else q) = q.
Proof.
  intros T x y p q neq.
  destruct (eq_id_dec x y).
    apply neq in e.
    contradiction.
  
   
   
   



 

 


(*
*** Local Variables: ***
*** coq-load-path: ("../book-sources") ***
*** End: ***
*)