Pull

Instructor/Exams/exam_1.lean

@@ -28,7 +28,8 @@ inductive binary_op : Type
 
 -- expressions (abstract syntax)
 inductive Expr : Type
--- Extra credit answers here
+| top_exp
+| bot_exp
 | var_exp (v : var)
 | un_exp (op : unary_op) (e : Expr)
 | bin_exp (op : binary_op) (e1 e2 : Expr)
@@ -74,7 +75,8 @@ def Interp := var → Bool
 
 -- The meanings of expressions "under" given interpretations
 def eval_expr : Expr → Interp → Bool 
--- Extra credit answers here
+| Expr.top_exp, _ => true
+| Expr.bot_exp, _ => false
 | (Expr.var_exp v),        i => i v
 | (Expr.un_exp op e),      i => (eval_un_op op) (eval_expr e i)
 | (Expr.bin_exp op e1 e2), i => (eval_bin_op op) (eval_expr e1 i) (eval_expr e2 i)
@@ -155,7 +157,8 @@ where mk_interps_helper : (rows : Nat) → (vars : Nat) → List Interp
 
 -- Count the number of variables in a given expression
 def max_variable_index : Expr → Nat
-| -- Extra credit answers here
+| Expr.top_exp => 1
+| Expr.bot_exp => 0
 | Expr.var_exp (var.mk i) => i
 | Expr.un_exp _ e => max_variable_index e
 | Expr.bin_exp _ e1 e2 => max (max_variable_index e1) (max_variable_index e2)
@@ -217,7 +220,7 @@ type α.
 -- Your answer here
 
 def and_elimination {α β : Type} : α × β → α 
-| (_, _) => _
+| (a, _) => a
 
 /-!
 ### b. Funny transitivity [15 points]
@@ -234,7 +237,7 @@ in this case.
 -- Your answer here
 
 def funny_transitivity {α β γ : Type} : (α → β) × (β → γ) → (α → γ)
-| _ => _
+| (a2b, b2y) => (fun a => b2y (a2b a))
 
 
 /-!
@@ -248,7 +251,7 @@ assumed value (a : α) one can always derive a value of
 -- Your answer here
 
 def ex_empty {α β : Type} : (α → Empty) → α → β
-| _, _ => _
+| a2e, a => nomatch (a2e a)
 
 /-!
 ## #2 Data Types
@@ -263,6 +266,17 @@ and the values of type Cheese are cheddar and brie.
 
 -- Your answers here
 
+inductive Bread : Type
+| white
+| wheat
+
+inductive Spread : Type
+| jam
+| pesto
+
+inductive Cheese : Type
+| cheddar
+| brie
 
 /-!
 ### b. An interesting inductive type [15 points]
@@ -277,6 +291,10 @@ the Sandwich type.
 -/
 
 -- Your answer here
+-- (s: (Cheese ⊕ Spread)) 
+structure Sandwich : Type := (c : Bread) (s: (Cheese ⊕ Spread))
+
+def v := Sandwich.mk Bread.white (Sum.inr Spread.jam)
 
 /-!
 ### c. Now make yourself a Sandwich [15 points]
@@ -289,7 +307,7 @@ bread and jam as a spread.
 
 -- Your answer here
 
-def jam_sandwich : Sandwich := _
+def jam_sandwich : Sandwich := Sandwich.mk Bread.wheat (Sum.inr Spread.jam)
 
 
 /-! 
@@ -321,7 +339,9 @@ as its arguments (1) type parameters (make them implicit),
 
 -- Your answer here
 
-
+def map {α β : Type} : (α → β) → List α → List β
+| _, [] => []
+| a2b, h::t => (a2b h) :: (map a2b t) 
 
 -- test case: use map instead of bit_list_to_bool_list
 -- expect [true, false, true, false, true]
@@ -348,7 +368,7 @@ Your job is to extend our syntax and semantics to include
 ⊤ and ⊥ as valid expressions. You will have to carry out
 the following tasks.
 
-- add top_exp and bot_exp as constructors in Expr
+- add true_exp and false_exp as constructors in Expr
 - note that we've already added concrete notation definitions
 - add rules for evaluating these expressions to eval_expr
 - add rules for these expressions to max_variable_index
@@ -367,5 +387,5 @@ Recall that a model is a binding of values to variables
 that makes a proposition true. What value must X have to
 make (X ⇒ ⊥) true?
 
--- Answer: {X is _____ } is a model of (X ⇒ ⊥)
+-- Answer: {X is false} is a model of (X ⇒ ⊥)
 -/

Instructor/Homework/hw3_key.lean

@@ -30,14 +30,15 @@ a result.
 
 -- Answer below
 
-def funkom : {α β γ : Type} → (β → γ) → (α → β) → (α → γ)
-| α, β, γ, g, f => fun (a : α) => (g (f a))
+
 
 /-!
 We'll implement a function of this type using what
 we call top-down type-guided structured programming.
 -/
 
+
+
 /-!
 Here's the procedure we followed when going over the HW.
 - introduce the name of the function with def
@@ -65,9 +66,6 @@ Define a function of the following polymorphic type:
 
 -- Answer below
 
-def mkop : {α β : Type} → (a : α) → (b : β) → α × β
-| α, β, a, b => (a,b) -- Prod.mk a b
-
 /-!
 We recommend the same top-down, type-guided structured
 programming approach. Some people would simply call it
@@ -84,9 +82,6 @@ Define a function of the following polymorphic type:
 
 -- Answer below
 
-def op_left : {α β : Type} → α × β → α
-| α, β, p => Prod.fst p
-
 -- Hint: Use top-down structured programming!
 
 
@@ -101,8 +96,6 @@ Define a function of the following polymorphic type:
 
 -- Hint: Use top-down structured programming
 
-def op_right {α β : Type} : α × β → β 
-| p => match p with | (_, b) => b
 
 
 /-! 
@@ -113,31 +106,12 @@ are the names of the seven days of the week: *sunday,
 monday,* etc. 
 -/
 
-inductive Day : Type
-|sunday
-|monday
-|tuesday
-|wednesday
-|thursday
-|friday
-|saturday
-
-open Day
-
-#check sunday
-
 /-!
 Some days are work days and some days are play
 days. Define a data type, *kind*, with two values,
 *work* and *play*.
 -/
 
-inductive kind : Type
-| work
-| play
-
-open kind
-
 /-!
 Now define a function, *day2kind*, that takes a *day*
 as an argument and returns the *kind* of day it is as
@@ -146,45 +120,23 @@ through friday) are *work* days and weekend days are
 *play* days.
 -/
 
-def day2kind : Day → kind 
-| sunday => play
-| saturday => play
-| _ => work
-
-#reduce day2kind thursday
-
 /-!
 Next, define a data type, *reward*, with two values,
 *money* and *health*.
 -/
 
-inductive reward : Type
-| money
-| health
-
-open reward
-
 /-!
 Now define a function, *kind2reward*, from *kind* to 
 *reward* where *reward work* is *money* and *reward play* 
 is *health*.
 -/
 
-def kind2reward : kind → reward
-| work => money
-| play => health
-
 /-!
 Finally, use your *funkom* function to produce a new
 function that takes a day and returns the corresponding
 reward. Call it *day2reward*.
 -/
 
-def day2reward := funkom kind2reward day2kind 
-
-#reduce day2reward tuesday
-#reduce day2reward saturday
-
 /-!
 Include test cases using #reduce to show that the reward
 from each weekday is *money* and the reward from a weekend
@@ -202,9 +154,6 @@ Consider the outputs of the following #check commands.
 #check Nat × (Nat × Nat)
 #check (Nat × Nat) × Nat
 
-#check (1,(2,3))
-#check ((1,2),3)
-
 /-!
 Is × left associative or right associative? Briefly explain
 how you reached your answer.
@@ -218,9 +167,6 @@ Define a function, *triple*, of the following type:
 
 -- Here:
 
-def triple : { α β γ : Type } → α → β → γ → (α × β × γ)
-| α, β, γ, a, b , y => (a,(b,y)) -- Prod.mk a (Prod.mk b y)
-
 -- Hints: (1) put in parens for clarity; (2) use TDSP.
 
 /-!
@@ -231,10 +177,7 @@ an argument and that returns, respectively, its first,
 second, or third elements.
 -/
 
--- Here
-
-def second { α β γ : Type } :  α × β × γ → β
-| (_,b,_) => b
+-- Here:
 
 -- Ok, this one takes a small leap of imagination
 

Instructor/Homework/hw5.lean

@@ -74,11 +74,12 @@ suggest that you go ahead and use *no* wherever
 doing so makes the logical meaning clearer. 
 -/
 def not_either_not_both { jam cheese } :
-  ((no jam) ⊕ (no cheese)) → 
-  (no (jam × cheese)) 
+  ((jam → Empty) ⊕ (cheese → Empty)) → 
+  (jam × cheese → Empty) 
 | Sum.inl nojam => (fun _ => _)
 | Sum.inr _ => _
 
+
 /-!
 ### #2: Not One or Not the Other Implies Not Both
 Now prove this principle *in general* by defining a 

Instructor/Homework/hw7_part2.lean

@@ -13,6 +13,8 @@ otherwise.
 
 -- Define your function here
 
+def pythag : Nat → Nat → Nat → Bool
+| a, b, c => if (a^2 + b^2 = c^2) then true else false
 
 -- The following test cases should then pass
 #eval pythag 3 4 5  -- expect true
@@ -29,7 +31,9 @@ inclusive.
 
 -- Define your function here
 
-
+def sum_cubes : Nat → Nat
+| 0 => 0
+| n' + 1 => (n'+1)^3 + sum_cubes n'
 
 
 -- test case: sum_cubes 4 = 1 + 8 + 27 + 64 = 100
@@ -59,13 +63,20 @@ Lean prover to work out a solution for each case.
 
 def prod_ors_to_or_prods {α β γ δ: Type} :
   (α ⊕ β) × (γ ⊕ δ) → α × γ ⊕ α × δ ⊕ β × γ ⊕ β × δ 
-| _ => _
-| _ => _
-| _ => _
-| _ => _
+| (Sum.inl a, Sum.inl c) => Sum.inl (a,c)
+| (Sum.inl a, Sum.inr d) => Sum.inr (Sum.inl (a,d))
+| (Sum.inr b, Sum.inl c) => Sum.inr (Sum.inr (Sum.inl (b,c)))
+| (Sum.inr b, Sum.inr d) => Sum.inr (Sum.inr (Sum.inr (b,d)))
 
 -- Write the second function here from scratch
 
+def or_prods_to_prod_ors {α β γ δ: Type} :
+  α × γ ⊕ α × δ ⊕ β × γ ⊕ β × δ → (α ⊕ β) × (γ ⊕ δ)
+| Sum.inl (a,c) => (Sum.inl a, Sum.inl c)
+| Sum.inr (Sum.inl (a,d)) => (Sum.inl a, Sum.inr d)
+| Sum.inr (Sum.inr (Sum.inl (b,c))) => (Sum.inr b, Sum.inl c)
+| Sum.inr (Sum.inr (Sum.inr (b,d))) => (Sum.inr b, Sum.inr d)
+
 /-!
 ## #4 Propositional Logic Syntax and Semantics
 
@@ -90,6 +101,8 @@ of propositional logic. Just write the expression
 here using the notation we've defined.
 -/
 
+-- def e := (A ∨ O) ∧ (C ∨ B) ⇔ ((A ∧ C) ∨ (A ∧ B) ∨ (O ∧ C) ∨ (O ∧ B))
+
 /-!
 ## #5 Propositional Logic Validity
 At the end of your updated Homework #7 file, use our

Instructor/Lectures/lecture_05.lean

@@ -232,7 +232,8 @@ otherwise.
 
 -- Answer here.
 
-def is_even_len := _  -- Be sure you can solve it
+def is_even_len := String → Bool
+  -- Be sure you can solve it
 
 #eval is_even_len "Love"    -- Expect true
 #eval is_even_len "Love!"   -- Expect false

Instructor/Lectures/lecture_12.lean

@@ -49,12 +49,6 @@ infixr:20 " ⇔ " => Expr.bin_exp binary_op.iff
 def eval_un_op : unary_op → (Bool → Bool)
 | unary_op.not => not
 
-
-def implies : Bool → Bool → Bool
-| true, false => false
-| _, _ => true
-
-
 def eval_bin_op : binary_op → (Bool → Bool → Bool)
 | binary_op.and => and
 | binary_op.or => or
@@ -217,13 +211,6 @@ First, define *b, c,* *j,* and *a* as propositional variables
 *cheese,* *j* for *jam,* and *a* for α*. 
 -/
 
-def b := var.mk 0
-def j := var.mk 1
-def c := var.mk 2
-def a := var.mk 3
-
--- get the index out of the c structure
-#eval c.n
 
 /-!
 ### #2. Atomic Propositions
@@ -232,11 +219,6 @@ Define B, C, J and A as corresponding atomic propositions,
 of type *Expr*. 
 -/
 
-def B := {b}     
-def C := {c}
-def J := {j}
-def A := {a}
-
 /-!
 ### #3. Compound Propositions