Set Implicit Arguments. Require Import Lia. Require Import Coq.Strings.String. Require Import Coq.Arith.PeanoNat. Require Import Coq.Arith.EqNat. Require Import Coq.Bool.Bool. From LF Require Export Basics. From LF Require Export Induction. (* Homework 1 *) (* Part 1: Recommended exercises *) Module Warmup. Theorem leb_refl : forall n:nat, (n <=? n) = true. Proof. Admitted. Theorem zero_neqb_S : forall n:nat, 0 =? (S n) = false. Proof. Admitted. Theorem andb_false_r : forall b : bool, andb b false = false. Proof. Admitted. Theorem S_neqb_0 : forall n:nat, (S n) =? 0 = false. Proof. Admitted. Theorem mult_1_l : forall n:nat, 1 * n = n. Proof. Admitted. Theorem all3_spec : forall b c : bool, orb (andb b c) (orb (negb b) (negb c)) = true. Proof. Admitted. Theorem mult_plus_distr_r : forall n m p : nat, (n + m) * p = (n * p) + (m * p). Proof. Admitted. Theorem mult_assoc : forall n m p : nat, n * (m * p) = (n * m) * p. Proof. Admitted. End Warmup. (* Part 2: Case Study - A language of simple arithmetic expressions *) Module SimpleArithmetic. Inductive exp : Set := | Const (v : nat) | Plus (e1 e2 : exp) | Minus (e1 e2 : exp) | Times (e1 e2 : exp). (* Examples. *) Example ex1 := Const 42. Example ex2 := Plus (Const 1) (Times (Const 2) (Const 3)). (* A function to compute the size of an arithmetic expression *) Fixpoint size (e : exp) : nat := match e with | Const _ => 1 | Plus e1 e2 => 1 + size e1 + size e2 | Minus e1 e2 => 1 + size e1 + size e2 | Times e1 e2 => 1 + size e1 + size e2 end. (* A function to compute the maximum height of an expression's AST *) Fixpoint height (e : exp) : nat := match e with | Const _ => 1 | Plus e1 e2 => 1 + max (height e1) (height e2) | Minus e1 e2 => 1 + max (height e1) (height e2) | Times e1 e2 => 1 + max (height e1) (height e2) end. Theorem height_to_size : forall e, height e <= size e. Proof. (* you may need to use the lia tactic in this proof. *) Admitted. (* A simple transformation over expressions - arguments can be swapped in commutative operations *) Fixpoint swap (e : exp) : exp := match e with | Const _ => e | Plus e1 e2 => Plus (swap e2) (swap e1) | Minus e1 e2 => Minus (swap e1) (swap e2) | Times e1 e2 => Times (swap e2) (swap e1) end. Theorem swap_preserves_size : forall e, size (swap e) = size e. Proof. Admitted. Theorem swap_preserves_depth_ : forall e, height (swap e) = height e. Proof. Admitted. (* Swapping twice yields the original expression *) Theorem swap_involutive : forall e, swap (swap e) = e. Proof. Admitted. End SimpleArithmetic. Module ArithWithVariables. Notation var := string. Definition var_eq : forall x y : var, {x = y} + {x <> y} := string_dec. Infix "==v" := var_eq (no associativity, at level 50). (* We now extend the language to support variables *) Inductive exp : Set := | Const (n : nat) | Var (x : var) | Plus (e1 e2 : exp) | Minus (e1 e2 : exp) | Times (e1 e2 : exp). Fixpoint size (e : exp) : nat := match e with | Const _ => 1 | Var _ => 1 | Plus e1 e2 => 1 + size e1 + size e2 | Minus e1 e2 => 1 + size e1 + size e2 | Times e1 e2 => 1 + size e1 + size e2 end. Fixpoint height (e : exp) : nat := match e with | Const _ => 1 | Var _ => 1 | Plus e1 e2 => 1 + max (height e1) (height e2) | Minus e1 e2 => 1 + max (height e1) (height e2) | Times e1 e2 => 1 + max (height e1) (height e2) end. (* This operator replaces all variable occurrences (subject) in an expression (org) with another expression (target) *) Fixpoint sub (org : exp) (subject : var) (target : exp) : exp := match org with | Const _ => org | Var x => if x ==v subject then target else org | Plus e1 e2 => Plus (sub e1 subject target) (sub e2 subject target) | Minus e1 e2 => Minus (sub e1 subject target) (sub e2 subject target) | Times e1 e2 => Times (sub e1 subject target) (sub e2 subject target) end. (* The swap function now extended to support variables *) Fixpoint swap (e : exp) : exp := match e with | Const _ => e | Var _ => e | Plus e1 e2 => Plus (swap e2) (swap e1) | Minus e1 e2 => Minus (swap e1) (swap e2) | Times e1 e2 => Times (swap e2) (swap e1) end. (* The height of an expression after substitution is never greater than the sum of the original and the target *) Theorem substitute_height : forall subject target org, height (sub org subject target) <= height org + height target. Proof. Admitted. (* Swapping and substitution are independent actions *) Theorem substitute_swap : forall subject target org, swap (sub org subject target) = sub (swap org) subject (swap target). Proof. Admitted. (* A simple transformation that replaces arithmetic operations with constant arguments by the value of the expression *) Fixpoint foldConstants (e : exp) : exp := match e with | Const _ => e | Var _ => e | Plus e1 e2 => let e1' := foldConstants e1 in let e2' := foldConstants e2 in match e1', e2' with | Const n1, Const n2 => Const (n1 + n2) | Const 0, _ => e2' | _, Const 0 => e1' | _, _ => Plus e1' e2' end | Minus e1 e2 => let e1' := foldConstants e1 in let e2' := foldConstants e2 in match e1', e2' with | Const n1, Const n2 => Const (n1 - n2) | Const 0, _ => Const 0 | _, Const 0 => e1' | _, _ => Plus e1' e2' end | Times e1 e2 => let e1' := foldConstants e1 in let e2' := foldConstants e2 in match e1', e2' with | Const n1, Const n2 => Const (n1 * n2) | Const 1, _ => e2' | _, Const 1 => e1' | Const 0, _ => Const 0 | _, Const 0 => Const 0 | _, _ => Times e1' e2' end end. (* The following proof can be solved using just the tactics discussed in class + lia * there are enough cases that this may be tedious. You're free to use tacticals * (like and ";" "try") to reduce proof burden, if you like, but it's not necessary * to complete the proof. *) (* Constant folding does not increase the size of an expression *) Theorem size_foldConstants: forall e, size (foldConstants e) <= size e. Proof. Admitted. (* An interpreter for arithmetic expressions *) (* A binding maps a variable to a value (here a natural number) *) Inductive binding : Type := | pair (x : var) (v : nat). (* A lookup table is either empty or contains a list of bindings *) Inductive lookupTable : Type := | empty | cons (b : binding) (l : lookupTable). (* This function looks up a variable (x) in a lookup table (l), and returns None if there is no binding for x in l, or Some v where v is the value in the binding (pair x v) found in l *) Fixpoint lookup (l : lookupTable) (x : var) : option nat := match l with | empty => None | cons (pair y v) l' => if (x ==v y) then Some v else lookup l' x end. (* A simple interpreter for our language *) Fixpoint interp (e : exp) (l : lookupTable) : nat := match e with | Const n => n | Var x => match (lookup l x) with | None => 0 | Some n => n end | Plus e1 e2 => interp e1 l + interp e2 l | Minus e1 e2 => interp e1 l - interp e2 l | Times e1 e2 => interp e1 l * interp e2 l end. (* Swapping arguments in commutative operations does not change the meaning of the expression *) Theorem swap_ok : forall l e, interp (swap e) l = interp e l. Proof. Admitted. (* Substituting an expression (target) whose interpretation is v for variable (target) in an expression (org) yields the same result when evaluated as binding target to v and evaluating org using that binding. *) Theorem sub_interp_ok : forall subject target org l v, interp target l = v -> lookup l subject = Some v -> interp (sub org subject target) l = interp org l. Proof. Admitted. End ArithWithVariables.