Semantics-Neapolis23: Lecture files

a1.v

Print bool.
Print nat.

(*
Inductive nat : Set :=
  O : nat
| S : nat -> nat.
(*a asdfads *)
asdfasdf
*)
Check 2.
Check (S (S (S O))).

(*
Inductive bool : Set :=
  true
| false
.
*)

Definition is_zero (n : nat) : bool :=
  match n with
  | O    => true 
  | S n' => false
  end.

Compute (is_zero O).
Compute (is_zero 0).
Compute (is_zero 5).

Definition is_zero' n :=
  match n with
  | O    => true 
  | S n' => false
  end.
Print is_zero'.

Definition is_zero'' (n : nat) :=
  match n with
  | 0 => true
  | S _ => false
  end.

Fail Definition is_odd n :=
  match n with
  | 0    => false
  | S n' => negb (is_odd n')
  end.

Fixpoint is_odd n :=
  match n with
  | 0       => false
  | 1       => true
  | S (S n) => is_odd n
  end.
Compute (is_odd 5).

Print list.
(*
Inductive list A :=
  nil
| cons (head : A) (tail : list A)
.
*)
Fail Fixpoint length l :=
  match l with
  | nil      => 0
  | cons _ l => 1 + length l
  end.

Fixpoint length'' (A : Type) (l : list A) :=
  match l with
  | nil      => 0
  | cons _ l => 1 + length'' A l
  end.

Fixpoint length' (A : Type) (l : list A) :=
  match l with
  | nil      => 0
  | cons _ l => 1 + length' _ l
  end.

Fixpoint length {A : Type} (l : list A) :=
  match l with
  | nil      => 0
  | cons _ l => 1 + length l
  end.

Compute (length (cons 5 nil)).
Compute (length (cons 5 (cons 7 nil))).

Require Import List.
Import ListNotations.

Compute (length [5; 7]).

Print option.
(* Inductive option (A : Type) : Type := *)
(* | None : option A *)
(* | Some : A -> option A. *)

Fixpoint max (l : list nat) : option nat :=
  match l with
  | nil => None 
  | cons a tl =>
      Some
        (match max tl with
         | None   => a
         | Some b => (Nat.max a b)
         end)
  end.
Compute (max []).
Compute (max [5;4;10;3]).

Definition max' (l : list nat)
  : option nat :=
  List.fold_left
    (fun m a =>
       match m with
       | None   => Some a
       | Some b => Some (Nat.max a b)
       end
    ) l None.
Compute (max' [1; 2]).

Module Attempt1.
Inductive tree A :=
| Empty
| Leaf (a : A)
| Node (a : A) (l : tree A) (r : tree A)
.

Fixpoint tree2list {A} (t : tree A)
  : list A :=
  match t with
  | Empty _  => []
  | Leaf  _ a => [a]
  | Node  _ a l r => tree2list l ++ [a]
                    ++ tree2list r
  end.
End Attempt1.

Set Implicit Arguments.

Inductive tree A :=
| Empty
| Leaf (a : A)
| Node (a : A) (l : tree A) (r : tree A)
.

Fixpoint tree2list {A} (t : tree A)
  : list A :=
  match t with
  | Empty _  => []
  | Leaf  a => [a]
  | Node  a l r => tree2list l ++ [a]
                    ++ tree2list r
  end.

Notation "'<|a, x, y|>'" := (@Node nat a x y).

a2.v

Theorem the_main_theorem1 : 2 * 2 = 4.
Proof.
  Locate "*".
  Print Nat.mul.
  Compute (2 * 2).
  Locate "=".
  simpl.
  Print eq.
  apply eq_refl.
Qed.
Print the_main_theorem1.
Definition the_main_theorem2 : 2 * 2 = 4 :=
  eq_refl.

Theorem the_main_theorem3 : 2 * 2 = 4.
Proof.
  apply eq_refl.
Qed.

Theorem the_main_theorem4 : 2 * 2 = 4.
Proof.
  reflexivity.
Qed.

Theorem the_main_theorem5 :
  exists x, x * 2 = 4.
Proof.
  exists 2.
  apply the_main_theorem1.
  (* reflexivity. *)
Qed.

Require Import List.
Import ListNotations.
Definition list123 : list nat := [1; 2; 3].
Theorem list123' : list nat.   
Proof.
  (* apply [1; 2; 3]. *)
  apply (cons 1 (cons 2 (cons 3 nil))).
Qed.

Theorem list123'' : list nat.   
Proof.
  (* Print list. *)
  (* apply nil. *)
  (* Print cons. *)
  apply cons.
  { apply 1. }
  apply cons.
  { apply 2. }
  apply cons.
  { apply 3. }
  apply nil.
Qed.
Print list123''.
Theorem the_main_theorem6 (AA : 2 * 2 = 5) :
  False.
Proof.
  rewrite the_main_theorem1 in AA at 1.
  inversion AA.
Qed.

Theorem the_main_theorem7 : False.
Proof.
  Print False.
Abort.

Theorem the_main_theorem8 (FF : False) :
  2 * 2 = 5.
Proof.
  (* inversion FF. *)
  destruct FF.
Qed.

Theorem length_of_non_empty_list
  (l : list nat) (NONEMPTY : l <> nil) :
  length l >0.
Proof.
  (* Print length. *)
  destruct l.
  { exfalso. red in NONEMPTY.
    apply NONEMPTY.
    reflexivity. }
  (* Locate ">". *)
  (* Print gt. *)
  (* Locate "<". *)
  (* Print lt. *)
  red. simpl.
  Search lt 0 S.
  apply PeanoNat.Nat.lt_0_succ.
Qed.

Require Import Lia.

Theorem length_of_non_empty_list'
  (l : list nat) (NONEMPTY : l <> nil) :
  length l > 0.
Proof.
  destruct l.
  2: { simpl. lia. }
  exfalso. red in NONEMPTY.
  apply NONEMPTY.
  reflexivity.
Qed.

a3.v

Require Import List.
Import ListNotations.
Require Import Lia.

Set Implicit Arguments.

Print list.
Print list_ind.

Inductive operation :=
| plus
| minus
| mult
| div 
| mod 
.
Print operation_ind.


Inductive expr :=
| Const (c : nat)
| Var   (v : list nat)
| BinOp (op : operation)
    (le : expr)
    (re : expr)
.
Print expr_ind.
Print length.

Lemma aaa x y
  (AA : x = 2)
  (BB : y = x) :
  x + y = 4.
Proof.
  subst.
  (* rewrite AA in BB. *)
  (* rewrite BB. *)
  simpl.
  (* Print eq. *)
  apply eq_refl.
  (* reflexivity. *)
Qed.

Lemma length_app {A} (l r : list A) :
  length (l ++ r) = length l + length r.
Proof.
  induction l.
  { simpl. (* apply eq_refl. *)
    reflexivity. }
  simpl.
  rewrite IHl.
  reflexivity.
Restart.
  (* induction l. *)
  (* all: simpl. *)
  induction l; simpl.
  2: rewrite IHl.
  all: reflexivity.
Restart.
  induction l; auto.
  simpl. rewrite IHl.
  auto.
Qed.

Inductive tree A :=
| Leaf (a : A)
| Node (a : A) (l : tree A) (r : tree A)
.

Fixpoint tree_height {A} (t : tree A) : nat :=
  match t with
  | Leaf _     => 1
  | Node _ l r => 1 + max (tree_height l)
                        (tree_height r)
  end.

Fixpoint tree_size {A} (t : tree A) : nat :=
  match t with
  | Leaf _     => 1
  | Node _ l r => 1 + tree_size l + tree_size r
  end.

Theorem tree_height_le_size {A} (t : tree A) :
  tree_height t <= tree_size t.
Proof.
  induction t; simpl.
  all: lia.
Qed.

Fixpoint tree2list {A} (t : tree A) :=
  match t with
  | Leaf a     => [a]
  | Node a l r => [a] ++ tree2list l ++ tree2list r
  end.

Theorem tree2list_length {A} (t : tree A) :
  length (tree2list t) = tree_size t.
Proof.
  induction t; simpl; auto.
  rewrite length_app.
  Print tree_ind.
  rewrite IHt1, IHt2; auto.
Qed.

ConstantFolding.v

Require Import BinInt ZArith_dec Zorder.
Require Export Id.
Require Export State.
Require Export Expr.

From hahn Require Import HahnBase.

Definition eval_op (op : bop) (z1 z2 : Z) : option Z :=
  match op with
  | Add => Some (z1 + z2)%Z
  | Sub => Some (z1 - z2)%Z
  | Mul => Some (z1 * z2)%Z
  | Div =>
    match z2 with
    | 0%Z => None
    | _   => Some (Z.div z1 z2)
    end
  | Mod =>
    match z2 with
    | 0%Z => None
    | _   => Some (Z.modulo z1 z2)
    end
  | Le =>
    match Ztrichotomy_inf z1 z2 with
    | inleft  _ => Some 1%Z
    | _ => Some 0%Z
    end
  | Lt =>
    match Ztrichotomy_inf z1 z2 with
    | inleft (left _) => Some 1%Z
    | _ => Some 0%Z
    end
  | Ge =>
    match Ztrichotomy_inf z1 z2 with
    | inleft (right _)
    | inright _ => Some 1%Z
    | _ => Some 0%Z
    end
  | Gt =>
    match Ztrichotomy_inf z1 z2 with
    | inright _ => Some 1%Z
    | _ => Some 0%Z
    end
  | Eq =>
    match Ztrichotomy_inf z1 z2 with
    | inleft (right _) => Some 1%Z
    | _ => Some 0%Z
    end
  | Ne =>
    match Ztrichotomy_inf z1 z2 with
    | inleft (right _) => Some 0%Z
    | _ => Some 1%Z
    end
  | And =>
    match z1, z2 with
    | 1%Z, 1%Z => Some 1%Z
    | 0%Z, 0%Z 
    | 0%Z, 1%Z
    | 1%Z, 0%Z => Some 0%Z
    | _, _ => None
    end
  | Or =>
    match z1, z2 with
    | 0%Z, 0%Z => Some 0%Z
    | 0%Z, 1%Z
    | 1%Z, 0%Z
    | 1%Z, 1%Z => Some 1%Z
    | _, _ => None
    end
  end.

Fixpoint cfold (e : expr) : expr :=
  match e with
  | Bop op e1 e2 =>
    let (c1, c2) := (cfold e1, cfold e2) in
    match c1, c2 with
    | Nat z1, Nat z2 =>
      match eval_op op z1 z2 with
      | Some v1 => Nat v1
      | _       => Bop op c1 c2
      end
    | _, _ => Bop op c1 c2
    end
  | _ => e
  end.

Lemma cfold_correct (e : expr) : cfold e ~e~ e.
Proof.
  assert (zbool 0) as Z0 by (red; intuition).
  assert (zbool 1) as Z1 by (red; intuition).
  induction e.
  1,2: by unfold cfold; apply eq_refl.
  red. ins.
  destruct (cfold e1) eqn:AA1.
  2,3: split; intros HH; inv HH;
    by econstructor; eauto; [apply IHe1|apply IHe2].
  destruct (cfold e2) eqn:AA2.
  3: { split; intros HH; inv HH.
       all: try by econstructor; eauto; [apply IHe1|apply IHe2].
       all: try by econstructor; [ | |eauto]; [apply IHe1|apply IHe2]. }
  2: { split; intros HH; inv HH.
       all: try by econstructor; eauto; [apply IHe1|apply IHe2].
       all: try by econstructor; [ | |eauto]; [apply IHe1|apply IHe2]. }
  destruct (eval_op b z z0) eqn:BB.
  2: { split; intros HH; inv HH.
       all: try by econstructor; eauto; [apply IHe1|apply IHe2].
       all: try by econstructor; [ | |eauto]; [apply IHe1|apply IHe2]. }
  unfold eval_op in *.
  split; intros HH.
  2: { assert (z1 = n); subst.
       2: by constructor.
       inv HH.
       all: desf;
         apply IHe1 in VALA; apply IHe2 in VALB; inv VALA; inv VALB; simpls.
       all: try by (try destruct s0); lia.
       all: unfold Z.eq in *; lia. }
  inv HH. desf.
  all: try by econstructor; eauto; [apply IHe1| apply IHe2];
    econstructor; eauto.
  all: try by econstructor; eauto; [apply IHe1|apply IHe2| desf];
    econstructor; eauto.
  all: try by econstructor; [apply IHe1 | apply IHe2| ]; eauto with semc;
    try (destruct s0); lia.
  all: try by econstructor; [apply IHe1|apply IHe2| ]; eauto with semc;
    unfold Z.eq in *; lia.
  all: try by
      match goal with
      | H1 : Nat ?v1 ~e~ ?e1,
        H2 : Nat ?v2 ~e~ ?e2 |- ([|?e1 [&] ?e2|] ?s => (?v)) =>
        assert ((v = v1 * v2)%Z) as BB by simpls; rewrite BB;
          constructor; auto; (try apply IHe1; eauto with semc);
            (try apply IHe2; eauto with semc)
      end.
  all: match goal with
       | H1 : Nat ?v1 ~e~ ?e1,
         H2 : Nat ?v2 ~e~ ?e2 |- ([|?e1 [\/] ?e2|] ?s => (?v)) =>
         assert ((v = zor v1 v2)%Z) as BB by simpls; rewrite BB;
           constructor; auto; (try apply IHe1; eauto with semc);
             (try apply IHe2; eauto with semc)
       end.
Qed.

Expr.v

Module SmokeTest.

  Lemma nat_always n (s : state Z) : [| Nat n |] s => n.
  (* Proof. apply bs_Nat. Qed. *)
  Proof. constructor. Qed.
  
  Lemma double_and_sum (s : state Z) (e : expr) (z : Z)
        (HH : [| e [*] (Nat 2) |] s => z) :
    [| e [+] e |] s => z.
  Proof.
    (* inversion HH; subst. *)
    inv HH.
    (* inversion VALB. subst. *)
    inv VALB.

    (* replace (za * 2)%Z with (za + za)%Z. *)
    (* 2: lia. *)
    replace (za * 2)%Z with (za + za)%Z by lia.

    (* apply bs_Add; apply VALA. *)
    (* apply bs_Add; assumption. *)
    (* apply bs_Add; auto. *)
    (* constructor; auto. *)
    auto with semc.
  Qed.
End SmokeTest.

State.v

  Lemma state_deterministic (st : state) (x : id) (n m : A)
        (SN : st / x => n)
        (SM : st / x => m) :
    n = m.
  Proof.
    (* induction st. *)
    (* { inversion SN. } *)
    (* destruct a as (x',n'). *)
    (* inversion SN. *)
    (* { subst. *)
    (*   inversion SM; subst; auto. *)
    (*   exfalso. apply H4. auto. } *)
    (* subst. *)
    (* inversion SM; subst. *)
    (* { exfalso. apply H4. auto. } *)
    (* apply IHst; auto. *)

    (* induction st; inv SN; inv SM *)
    (* all: inversion SM; subst; auto. *)
    (* all: exfalso; auto. *)

    induction st; inv SN; inv SM; auto.
  Qed.