Code from class on Feb 20 (CS691PL)

Feb20.v

Set Implicit Arguments.

Module Semantics.

  Inductive binop : Set := Plus | Times.
  
  Inductive exp : Set :=
  | Const : nat -> exp
  | Binop : binop -> exp -> exp -> exp.
  
  Definition binopDenote (b : binop) : nat -> nat -> nat :=
    match b with
      | Plus => plus
      | Times => mult
    end.
  
  Fixpoint expDenote (e : exp) : nat :=
    match e with
      | Const n => n
      | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2)
    end.

  Inductive step : exp -> exp -> Prop :=
  | binop_red : forall (m n : nat) (b : binop), 
                  step (Binop b (Const m) (Const n)) (Const (binopDenote b m n))
  | binop_1 :
      forall b e1 e1' e2,
        step e1 e1' ->
        step (Binop b e1 e2) (Binop b e1' e2)
  | binop_2 :
      forall b n e e',
        step e e' ->
        step (Binop b (Const n) e) (Binop b (Const n) e')
  | trans :
      forall e1 e2 e3,
        step e1 e2 ->
        step e2 e3 ->
        step e1 e3.

  Definition ex1 := Binop Plus (Binop Times (Const 3) (Const 2)) (Const 5).

  Eval compute in expDenote ex1.

  Example ex1_step_correct : step ex1 (Const 11).
    unfold ex1.
    eapply trans.
    apply binop_1.
    apply binop_red.
    apply binop_red.
  Qed.

  Hint Constructors step.

  Example ex1_step_correct_eauto : step ex1 (Const 11).
  unfold ex1.
  eauto 20.
  (* eauto 20 does not work. *)
  Abort.

  Lemma binop_result : 
    forall b m n r, 
      r = binopDenote b m n  -> 
      step (Binop b (Const m) (Const n)) (Const r).
    intros.
    rewrite H.
    constructor.
  Qed.

  Hint Resolve binop_result.

  Example ex1_step_correct_eauto : step ex1 (Const 11).
  unfold ex1.
  eauto 4.
  Qed.

End Semantics.

Module TypeInference.

  Require Import List.

  (* Gives the :: notation for cons *)
  Import ListNotations.
  
  (* Expressions with de Brujin indices *)
  Inductive exp : Set :=
  | Var : nat -> exp
  | Fun : exp -> exp
  | Nat : nat -> exp
  | App : exp -> exp -> exp.

  Inductive typ : Set :=
  | TyNat : typ
  | TyArr : typ -> typ -> typ.

  Definition env := list typ.

  Inductive Nth (A : Type) : nat -> list A -> A -> Prop :=
  | Head : forall x xs, Nth 0 (x :: xs) x
  | Tail : forall n x y xs,
             Nth n xs x ->
             Nth (S n) (y :: xs) x.

  Inductive typing : env -> exp -> typ -> Prop :=
  | TNat : forall env n, typing env (Nat n) TyNat
  | TApp : forall env t1 t2 e1 e2, 
             typing env e1 (TyArr t1 t2) ->
             typing env e2 t1 ->
             typing env (App e1 e2) t2
  | TAbs : forall env t1 t2 e,
             typing (t1 :: env) e t2 ->
             typing env (Fun e) (TyArr t1 t2)
  | TVar : forall env t k, Nth k env t -> typing env (Var k) t.

  Hint Constructors Nth typing typ exp.

  Example typing_id : typing nil (App (Fun (Var 0)) (Nat 10)) TyNat.
  eauto.
  Qed.
  Print typing_id.

  Example typing_id' : exists t, typing nil (App (Fun (Var 0)) (Nat 10)) t.
  eauto.
  Qed.

  Example typing_ex2 :  typing nil (App (Fun (App (Var 0) (Nat 10))) (Fun (Var 0))) TyNat.
  intros.
  eauto 8.
  Qed.

  Example typing_app :  typing nil 
                               (App 
                                  (App (Fun (Fun (App (Var 1) (Var 0))))
                                       (Fun (Var 0)))
                                  (Nat 10))
                               TyNat.
  intros.
  eauto 12.
  Qed.

End TypeInference.