UVa CS2120-002 F23 Midterm Exam

The first section of this exam just repeats our definition of propositional logic syntax and semantics. Skip ahead to the second section to find the exam.

Propositional Logic: Syntax, Sematics, Satisfiability

This section of the exam simply includes our formal definition of the syntax and semantics of propositional logic and of functions that determine whether a given expression is valid, satisfiable, or unsatisfiable.

Syntax

-- variables
structure var : Type :=  (n: Nat)

-- connectives/operators
inductive unary_op : Type | not
inductive binary_op : Type
| and
| or
| imp
| iff

-- expressions (abstract syntax)
inductive Expr : Type
-- Extra credit answers here
| var_exp (v : var)
| un_exp (op : unary_op) (e : Expr)
| bin_exp (op : binary_op) (e1 e2 : Expr)

-- concrete syntax 
notation "{"v"}" => Expr.var_exp v
prefix:max "¬" => Expr.un_exp unary_op.not 
infixr:35 " ∧ " => Expr.bin_exp binary_op.and  
infixr:30 " ∨ " => Expr.bin_exp binary_op.or 
infixr:25 " ⇒ " =>  Expr.bin_exp binary_op.imp
infixr:20 " ⇔ " => Expr.bin_exp binary_op.iff 
notation " ⊤ " => Expr.top_exp
notation " ⊥ " => Expr.bot_exp

Semantics

-- meanings of unary operators
def eval_un_op : unary_op → (Bool → Bool)
| unary_op.not => not

-- missing binary Boolean operators
def implies : Bool → Bool → Bool
| true, false => false
| _, _ => true

def iff : Bool → Bool → Bool
| true, true => true
| false, false => true
| _, _ => false

-- meanings of binary operators
def eval_bin_op : binary_op → (Bool → Bool → Bool)
| binary_op.and => and
| binary_op.or => or
| binary_op.imp => implies
| binary_op.iff => iff

-- The interpretation type
def Interp := var → Bool 

-- The meanings of expressions "under" given interpretations
def eval_expr : Expr → Interp → Bool 
-- Extra credit answers here
| (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)

Satisfiability

We built a satisfiability checker for propositional logic, in several pieces. This subsection includes all definitions.

Truth Table Input Rows

-- Nat to Binary
-- You don't need to worry about the "have" part
def right_bit (n : Nat) := n%2
def shift_right (n : Nat) := n/2
def 
Warning: declaration uses 'sorry'
Warning: declaration uses 'sorry'
 : 
Nat: Type
Nat → 
List: Type → Type
List 
Nat: Type
Nat
| 
0: Nat
0     => [
0: Nat
0]
| 
1: Nat
1     => [
1: Nat
1]
| 
n': Nat
n' + 2 =>
  have : (
shift_right: Nat → Nat
shift_right (
n': Nat
n' + 
2: Nat
2)) < (
n': Nat
n' + 
2: Nat
2) := 
sorry: shift_right (n' + 2) < n' + 2
sorry
  
nat_to_bin: Nat → List Nat
nat_to_bin (
shift_right: Nat → Nat
shift_right (
n': Nat
n' + 
2: Nat
2)) ++ [
right_bit: Nat → Nat
right_bit (
n': Nat
n' + 
2: Nat
2)]

-- Left pad with zeros
def 
zero_pad: Nat → List Nat → List Nat
zero_pad : 
Nat: Type
Nat → 
List: Type → Type
List 
Nat: Type
Nat → 
List: Type → Type
List 
Nat: Type
Nat
  | 
v: Nat
v, 
l: List Nat
l => 
zero_pad_recursive: Nat → List Nat → List Nat
zero_pad_recursive (
v: Nat
v - (
l: List Nat
l.
length: {α : Type} → List α → Nat
length)) 
l: List Nat
l
where 
zero_pad_recursive: Nat → List Nat → List Nat
zero_pad_recursive : 
Nat: Type
Nat → 
List: Type → Type
List 
Nat: Type
Nat → 
List: Type → Type
List 
Nat: Type
Nat
  | 
0: Nat
0, 
l: List Nat
l => 
l: List Nat
l
  | 
v': Nat
v'+1, 
l: List Nat
l => 
zero_pad_recursive: Nat → List Nat → List Nat
zero_pad_recursive 
v': Nat
v' (
0: Nat
0::
l: List Nat
l)

-- Make row of bits at index "row" padded out to "cols" wide 
def 
mk_bit_row: Nat → Nat → List Nat
mk_bit_row : (
row: Nat
row: 
Nat: Type
Nat) → (
cols: Nat
cols : 
Nat: Type
Nat) → 
List: Type → Type
List 
Nat: Type
Nat
| 
r: Nat
r, 
c: Nat
c => 
zero_pad: Nat → List Nat → List Nat
zero_pad 
c: Nat
c (
nat_to_bin: Nat → List Nat
nat_to_bin 
r: Nat
r)

-- Convert list of bits to list of bools
def 
bit_to_bool: Nat → Bool
bit_to_bool : 
Nat: Type
Nat → 
Bool: Type
Bool
| 
0: Nat
0 => 
false: Bool
false
| _ => 
true: Bool
true

def 
bit_list_to_bool_list: List Nat → List Bool
bit_list_to_bool_list : 
List: Type → Type
List 
Nat: Type
Nat → 
List: Type → Type
List 
Bool: Type
Bool
| [] => 
[]: List Bool
[]
| 
h: Nat
h::
t: List Nat
t => (
bit_to_bool: Nat → Bool
bit_to_bool 
h: Nat
h) :: (
bit_list_to_bool_list: List Nat → List Bool
bit_list_to_bool_list 
t: List Nat
t)

-- Make row'th row of truth table with vars variables
def 
mk_row_bools: Nat → Nat → List Bool
mk_row_bools : (
row: Nat
row : 
Nat: Type
Nat) → (
vars: Nat
vars : 
Nat: Type
Nat) → 
List: Type → Type
List 
Bool: Type
Bool
| 
r: Nat
r, 
v: Nat
v => 
bit_list_to_bool_list: List Nat → List Bool
bit_list_to_bool_list (
mk_bit_row: Nat → Nat → List Nat
mk_bit_row 
r: Nat
r 
v: Nat
v)

Interpretations

-- Convert list of bools to interpretation
def 
override: Interp → var → Bool → Interp
override : 
Interp: Type
Interp → 
var: Type
var → 
Bool: Type
Bool → 
Interp: Type
Interp
| 
old_interp: Interp
old_interp, 
var: _root_.var
var, 
new_val: Bool
new_val => 
  (λ 
v: _root_.var
v => if (
v: _root_.var
v.
n: _root_.var → Nat
n == 
var: _root_.var
var.
n: _root_.var → Nat
n)     -- when applied to var
          then 
new_val: Bool
new_val          -- return new value
          else 
old_interp: Interp
old_interp 
v: _root_.var
v)  -- else retur old value

def 
bools_to_interp: List Bool → Interp
bools_to_interp : 
List: Type → Type
List 
Bool: Type
Bool → 
Interp: Type
Interp
  | 
l: List Bool
l => 
bools_to_interp_helper: Nat → List Bool → Interp
bools_to_interp_helper 
l: List Bool
l.
length: {α : Type} → List α → Nat
length 
l: List Bool
l
where 
bools_to_interp_helper: Nat → List Bool → Interp
bools_to_interp_helper : (
vars: Nat
vars : 
Nat: Type
Nat) → (
vals: List Bool
vals : 
List: Type → Type
List 
Bool: Type
Bool) → 
Interp: Type
Interp
  | _, [] => (λ 
_: var
_ => 
false: Bool
false)
  | 
vars: Nat
vars, 
h: Bool
h::
t: List Bool
t =>
    let 
len: Nat
len := (
h: Bool
h::
t: List Bool
t).
length: {α : Type} → List α → Nat
length
    
override: Interp → var → Bool → Interp
override (
bools_to_interp_helper: Nat → List Bool → Interp
bools_to_interp_helper 
vars: Nat
vars 
t: List Bool
t) (
var.mk: Nat → var
var.mk (
vars: Nat
vars - 
len: Nat
len)) 
h: Bool
h 

-- Make an interpretation for given row with "vars" variables
def 
mk_interp_vars_row: Nat → Nat → Interp
mk_interp_vars_row : (
vars: Nat
vars: 
Nat: Type
Nat) → (
row: Nat
row: 
Nat: Type
Nat) → 
Interp: Type
Interp
| 
v: Nat
v, 
r: Nat
r => 
bools_to_interp: List Bool → Interp
bools_to_interp (
mk_row_bools: Nat → Nat → List Bool
mk_row_bools 
r: Nat
r 
v: Nat
v)

-- Given number of variables, return list of interpretations
def 
mk_interps: Nat → List Interp
mk_interps (
vars: Nat
vars : 
Nat: Type
Nat) : 
List: Type → Type
List 
Interp: Type
Interp := 
  
mk_interps_helper: Nat → Nat → List Interp
mk_interps_helper (
2: Nat
2^
vars: Nat
vars) 
vars: Nat
vars
where 
mk_interps_helper: Nat → Nat → List Interp
mk_interps_helper : (
rows: Nat
rows : 
Nat: Type
Nat) → (
vars: Nat
vars : 
Nat: Type
Nat) → 
List: Type → Type
List 
Interp: Type
Interp
  | 
0: Nat
0, _         => 
[]: List Interp
[]
  | (
n': Nat
n' + 1), 
v: Nat
v  => (
mk_interp_vars_row: Nat → Nat → Interp
mk_interp_vars_row 
v: Nat
v 
n': Nat
n')::
mk_interps_helper: Nat → Nat → List Interp
mk_interps_helper 
n': Nat
n' 
v: Nat
v

-- Count the number of variables in a given expression
def 
max_variable_index: Expr → Nat
max_variable_index : 
Expr: Type
Expr → 
Nat: Type
Nat
| -- Extra credit answers here
| 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)

def 
num_vars: Expr → Nat
num_vars : 
Expr: Type
Expr → 
Nat: Type
Nat := λ 
e: Expr
e => 
max_variable_index: Expr → Nat
max_variable_index 
e: Expr
e + 
1: Nat
1

Truth Table Output Column

def 
eval_expr_interps: List Interp → Expr → List Bool
eval_expr_interps : 
List: Type → Type
List 
Interp: Type
Interp → 
Expr: Type
Expr → 
List: Type → Type
List 
Bool: Type
Bool
| [], _ => 
[]: List Bool
[]
| 
h: Interp
h::
t: List Interp
t, 
e: Expr
e => 
eval_expr_interps: List Interp → Expr → List Bool
eval_expr_interps 
t: List Interp
t 
e: Expr
e ++ [
eval_expr: Expr → Interp → Bool
eval_expr 
e: Expr
e 
h: Interp
h]

-- Given expression, return truth table outputs by ascending row index
def 
truth_table_outputs: Expr → List Bool
truth_table_outputs : 
Expr: Type
Expr → 
List: Type → Type
List 
Bool: Type
Bool
| 
e: Expr
e =>  
eval_expr_interps: List Interp → Expr → List Bool
eval_expr_interps (
mk_interps: Nat → List Interp
mk_interps (
num_vars: Expr → Nat
num_vars 
e: Expr
e)) 
e: Expr
e

Reducers: Boolean List to Bool with And and Or

-- functions to check if bool list has any, resp. all, values true
def 
reduce_or: List Bool → Bool
reduce_or : 
List: Type → Type
List 
Bool: Type
Bool → 
Bool: Type
Bool 
| [] => 
false: Bool
false
| 
h: Bool
h::
t: List Bool
t => 
or: Bool → Bool → Bool
or 
h: Bool
h (
reduce_or: List Bool → Bool
reduce_or 
t: List Bool
t)

def 
reduce_and: List Bool → Bool
reduce_and : 
List: Type → Type
List 
Bool: Type
Bool → 
Bool: Type
Bool 
| [] => 
true: Bool
true
| 
h: Bool
h::
t: List Bool
t => 
and: Bool → Bool → Bool
and 
h: Bool
h (
reduce_and: List Bool → Bool
reduce_and 
t: List Bool
t)

Satisfiability Checkers

-- Three main functions: test given expression for satsfiability properties
def 
is_sat: Expr → Bool
is_sat : 
Expr: Type
Expr → 
Bool: Type
Bool := λ 
e: Expr
e : 
Expr: Type
Expr => 
reduce_or: List Bool → Bool
reduce_or (
truth_table_outputs: Expr → List Bool
truth_table_outputs 
e: Expr
e)
def 
is_valid: Expr → Bool
is_valid : 
Expr: Type
Expr → 
Bool: Type
Bool := λ 
e: Expr
e : 
Expr: Type
Expr => 
reduce_and: List Bool → Bool
reduce_and (
truth_table_outputs: Expr → List Bool
truth_table_outputs 
e: Expr
e)
def 
is_unsat: Expr → Bool
is_unsat : 
Expr: Type
Expr → 
Bool: Type
Bool := λ 
e: Expr
e : 
Expr: Type
Expr => 
not: Bool → Bool
not (
is_sat: Expr → Bool
is_sat 
e: Expr
e)

EXAM STARTS HERE

#1 Proofs as Programs

a. And elimination [15 points]

Prove, by completing the following function definition, that from a value of type α × β one can always derive a value of type α.

-- Your answer here

def 
and_elimination: {α β : Type} → α × β → α
and_elimination {
α: Type
α 
β: Type
β : 
Type: Type 1
Type} : 
α: Type
α × 
β: Type
β → 
α: Type
α 
| (_, _) => 
Error: don't know how to synthesize placeholder
context:
α β : Type
fst✝ : α
snd✝ : β
⊢ α

b. Funny transitivity [15 points]

Prove, by completing the following function definition, that (α → β) × (β → γ) → (α → γ). In other words, if you have a pair of functions, one converting α to β and one converting β to γ, then you can always construct a function from α to γ. Hint: Use type-guided top-down programming, and remember how to express a function value: that's what you have to return in this case.

-- Your answer here

def funny_transitivity {α β γ : Type} : (α → β) × (β → γ) → (α → γ)
| _ => 
Error: don't know how to synthesize placeholder
context:
α β γ : Type
x✝ : (α → β) × (β → γ)
⊢ α → γ

c. Ex empty quodlibet [15 points]

Prove that if a type, α, is uninhabited then from an assumed value (a : α) one can always derive a value of any type, β. 

-- Your answer here

def ex_empty {α β : Type} : (α → Empty) → α → β
| _, _ => 
Error: don't know how to synthesize placeholder
context:
α β : Type
x✝¹ : α → Empty
x✝ : α
⊢ β

#2 Data Types

a. Enumerated Types [10 points]

Define three enumerated types, called Bread, Spread, and Cheese, where the values of type Bread are white and wheat; the values of type Spread are jam and pesto; and the values of type Cheese are cheddar and brie.

-- Your answers here

b. An interesting inductive type [15 points]

Define a data type called Sandwich, with one constructor called mk, taking as its arguments a choice of bread and either (but not both) a choice of Cheese or a choice of Spread. Hint: Remember how to define a type that carries a value of either one type or another. Extra credit [2pts] for using structure instead of inductive to declare the Sandwich type.

-- Your answer here

c. Now make yourself a Sandwich [15 points]

Define jam_sandwhich to be a Sandwhich made with wheat bread and jam. You have to use Sandwich.mk to create a term representing a sandwich with wheat bread and jam as a spread.

-- Your answer here

def jam_sandwich : Sandwich := 
Error: don't know how to synthesize placeholder
context:
Sandwich : Sort u_1
⊢ Sandwich

#3 Recursive Data and Functions [15 points]

In our implementation of propositional logic, we defined a function, bit_list_to_bool_list, to convert a list of Nat to a corresponding list of Bool. Here's the definition (with a tick mark on the name).

def 
bit_list_to_bool_list': List Nat → List Bool
bit_list_to_bool_list' : 
List: Type → Type
List 
Nat: Type
Nat → 
List: Type → Type
List 
Bool: Type
Bool
| [] => 
[]: List Bool
[]
| 
h: Nat
h::
t: List Nat
t => (
bit_to_bool: Nat → Bool
bit_to_bool 
h: Nat
h) :: (
bit_list_to_bool_list: List Nat → List Bool
bit_list_to_bool_list 
t: List Nat
t)

-- expect [true, false, true, false, true]

[true, false, true, false, true]

 
bit_list_to_bool_list: List Nat → List Bool
bit_list_to_bool_list [
1: Nat
1, 
0: Nat
0, 
3: Nat
3, 
0: Nat
0, 
1: Nat
1]

Your job is to generalize this solution by defining a new function, called map. Generalize the types, Nat and Bool, to arbitrary types, α and β. Generalize bit_to_bool to be any function for converting an individual α value into a corresponding β value. Your map function will thus take as its arguments (1) type parameters (make them implicit), (2) a function for converting elements, and (3) a List of α values, and will return a correspond List of β values.

-- Your answer here



-- test case: use map instead of bit_list_to_bool_list
-- expect [true, false, true, false, true]
#eval 
Error: unknown identifier 'map'
 bit_to_bool [1, 0, 1, 0, 1]: ?m.44293
 bit_to_bool [1, 0, 1, 0, 1]

#4 Propositional Logic [10 pts Extra Credit, for A+]

Propositional logic as we've formulate it has variable expressions (atomic expressions), and larger expressions built by applying connectives (∧, ∨, ¬, ⇒, ⇔) to smaller expressions.

Some formalizations of propositional logic also include the constant expressions True and False. In concrete syntax, they are sometimes written as ⊤ (pronounced top) and ⊥ (bottom). Semantically ⊤ evaluates to Boolean true and ⊥ evaluates to Boolean false.

a. Extend Syntax and Semantics

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
  • 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

When you're done, the following logic should evaluate without error.

def 
X: Expr
X := {
var.mk: Nat → var
var.mk 
0: Nat
0}

Error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
 
Error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
Error: unknown constant 'Expr.bot_exp'
Error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
  -- expect true

b. Give a model for (X ⇒ ⊥)

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 ⇒ ⊥)