Repeat exam 2018–2019


Question 1

1a

inductive big_step : pl σ × σ → string × σ → Prop
| skip {s} :
  big_step (skip, s) ("", s)
| print {m s} :
  big_step (print m, s) (m, s)
| seq {p₁ p₂ s u} o₁ o₂ t (h₁ : big_step (p₁, s) (o₁, t)) (h₂ : big_step (p₂, t) (o₂, u)) :
  big_step (seq p₁ p₂, s) (o₁ ++ o₂, u)

1b

inductive small_step : pl σ × (string × σ) → pl σ × (string × σ) → Prop
| print {m m' s}:
  small_step (print m', (m, s)) (skip, (m ++ m', s))
| seq_step {p₁ p₂ ms ms'} (p) :
  small_step (p₁, ms) (p, ms') → small_step (seq p₁ p₂, ms) (seq p p₂, ms')
| seq_skip {p s} :
  small_step (seq skip p, s) (p, s)

1c

def program_equiv (p₁ p₂ : pl σ) : Prop :=
∀s mt, (p₁, s) ⟹ mt ↔ (p₂, s) ⟹ mt

local infix ` ≈ ` := program_equiv

1. They are in general not the same. `while (λ_, true) skip` never terminates,
hences it never leads to some state `mt`, whereas `skip` will always terminate.

2. If we start in a state `s`, executing the lhs yields the state obtained after executing p, then q, then r, in that order. This is the same in the rhs.

3. Counterexample: Any `m` that is not the empty string.


Question 2

2a

def map_tree {α β : Type} (f : α → β) : tree α → tree β
| empty         := empty
| (bin a l r)   := bin (f a) (map_tree l) (map_tree r)
| (ter a l m r) := ter (f a) (map_tree l) (map_tree m) (map_tree r)

2b

lemma map_tree_id {α : Type} :
  ∀t : tree α, map_tree (λx : α, x) t = t
| empty         := by refl
| (bin a l r)   := by simp [map_tree, map_tree_id l, map_tree_id r]
| (ter a l m r) := by simp [map_tree, map_tree_id l, map_tree_id m, map_tree_id r]

2c

def set_tree {α : Type} : tree α → set α
| empty         := ∅
| (bin a l r)   := insert a (set_tree l ∪ set_tree r)
| (ter a l m r) := insert a (set_tree l ∪ set_tree m ∪ set_tree r)

2d

lemma map_tree_congr_strong {α β : Type} (f g : α → β) :
  ∀t : tree α, (∀x, x ∈ set_tree t → f x = g x) → map_tree f t = map_tree g t
| empty         := by intros; refl
| (bin a l r)   :=
  begin
    intros,
    simp [map_tree],
    repeat { apply and.intro },
    { apply a_1, simp [set_tree], sorry },
    { apply map_tree_congr_strong, intros, apply a_1, simp [set_tree], sorry },
    { apply map_tree_congr_strong, intros, apply a_1, simp [set_tree], sorry }
  end
| (ter a l m r)   :=
  /- similar to bin case but with three invocations of the induction
     hypothesis -/


Question 3

3a

Sound? Yes. The rule is sound. Proof sketch:

    * P holds at the beginning (precondition of conclusion).
    * If c is true, then P holds before executing the body p.
    * By the hypothesis, P holds after executing the body p. It is a loop
      invariant.
    * Hence P holds before the second loop iteration.
    * If c is false, we may assume that P holds (since it is a loop invariant),
      and we know that c is false. Hence the postcondition of `while` is
      justified.

Complete? No, because the hypothesis could assume that c is true, which it
does not.

3b

Alyssa P. Hacker is right. Given a Hoare triple {P}p{Q}, you can always make
the precondition more restrictive or the postcondition less restrictive. In
both cases, it reduces the expressivity of the triple. The least expressive
triple is {false}p{true}.

3c

lemma ite_intro_ela (h₁ : {* R₁ *} p₁ {* S *}) (h₂ : {* R₂ *} p₂ {* S *}) :
  {* λs, (c s ∧ R₁ s) ∨ (¬ c s ∧ R₂ s) *} ite c p₁ p₂ {* S *}
:= sorry

lemma ite_intro (h₁ : {* λs, P s ∧ c s *} p₁ {* Q *}) (h₂ : {* λs, P s ∧ ¬ c s *} p₂ {* Q *}) :
  {* P *} ite c p₁ p₂ {* Q *}
:=
begin
  have p_eq : P = λs, (c s ∧ P s) ∨ (¬ c s ∧ P s) :=
    begin
      apply funext,
      intro s,
      rw ← iff_eq_eq,
      apply iff.intro,
      intro ps,
      apply classical.by_cases,
      intro h,
      apply or.intro_left,
      apply and.intro,
      apply h,
      apply ps,
      intro h,
      apply or.intro_right,
      apply and.intro,
      apply h,
      apply ps,
      intro h,
      cases h,
      cases h,
      apply h_right,
      cases h,
      apply h_right
    end,
  have p_eq' : P = λs, (c s ∧ (P s ∧ c s)) ∨ (¬ c s ∧ (P s ∧ ¬ c s)) :=
    begin
      -- rw p_eq,
      apply funext,
      intro x,
      rw @and.comm _ (c x),
      sorry
    end,
  rw p_eq',
  apply ite_intro_ela,
  apply h₁,
  apply h₂
end

lemma ite_intro_ela' (h₁ : {* R₁ *} p₁ {* S *}) (h₂ : {* R₂ *} p₂ {* S *}) :
  {* λs, (c s ∧ R₁ s) ∨ (¬ c s ∧ R₂ s) *} ite c p₁ p₂ {* S *} :=
begin
  apply ite_intro,
  apply consequence_left,
  assumption,
  intros,
  cases a,
  cases a_left,
  cases a_left,
  assumption,
  cases a_left,
  contradiction,
  apply consequence_left,
  assumption,
  intros,
  cases a,
  cases a_left,
  cases a_left,
  contradiction,
  cases a_left,
  assumption
end


Question 4

4a

inductive is_binary {α : Type} : tree α → Prop
| empty       : is_binary empty
| bin {a l r} : is_binary l → is_binary r → is_binary (bin a l r)

4b

lemma is_binary_map_tree {α β : Type} {f : α → β} :
  ∀{t : tree α}, is_binary t → is_binary (map_tree f t)
| empty       h := is_binary.empty
| (bin a l r) h :=
  begin
    cases h,
    apply is_binary.bin,
    apply is_binary_map_tree,
    assumption,
    apply is_binary_map_tree,
    assumption
  end

4c

def btree (α : Type) : Type := {t : tree α // is_binary t}

4d

def empty_btree {α : Type} : btree α :=
⟨empty, is_binary.empty⟩

def bin_btree {α : Type} (a : α) (l r : btree α) : btree α :=
⟨bin a l.1 r.1, is_binary.bin l.2 r.2⟩

4e

def set_btree {α : Type} (t : btree α) : set α :=
set_tree t.1

def map_btree {α β : Type} (f : α → β) (t : btree α) : btree β :=
⟨map_tree f t.1, is_binary_map_tree t.2⟩


Question 5

5a

inductive rsc {α : Type} (r : α → α → Prop) : α → α → Prop
| base : ∀a b, r a b → rsc a b
| refl : ∀a, rsc a a
| symm : ∀a b, rsc a b → rsc b a

5b

lemma refl_symm_imp_rsc_iff {α : Type} {r : α → α → Prop}
  (refl_r : ∀a, r a a) (symm_r : ∀a b, r a b → r b a) :
  ∀a b, rsc r a b ↔ r a b :=
begin
  intros,
  apply iff.intro,
  { intro cab,
    induction cab,
    { assumption },
    { apply refl_r },
    { apply symm_r, apply cab_ih } },
  {
    intro rab,
    apply rsc.base,
    apply rab
  }
end

5c

lemma rsc_rsc_iff_rsc {α : Type} {r : α → α → Prop} :
  ∀a b : α, rsc (rsc r) a b ↔ rsc r a b :=
begin
  intros,
  apply refl_symm_imp_rsc_iff,
  intro a,
  apply rsc.refl,
  intros a b,
  apply rsc.symm
end
