Final exam 2018–2019


Question 1

1a

inductive tc₂ {α : Type} (r : α → α → Prop) : α → α → Prop
| base     : ∀a b, r a b → tc₂ a b
| pets : ∀a b c, tc₂ a b → r b c → tc₂ a c

1b

inductive tc₃ {α : Type} (r : α → α → Prop) : α → α → Prop
| base  : ∀a b, r a b → tc₃ a b
| trans : ∀a b c, tc₃ a b → tc₃ b c → tc₃ a c

1c

lemma tc₃_step {α : Type} (r : α → α → Prop) (a b c : α) (rab : r a b) (tbc : tc₃ r b c) :
  tc₃ r a c :=
tc₃.trans _ _ _ (tc₃.base _ _ rab) tbc

1d

lemma tc₁_pets {α : Type} (r : α → α → Prop) (c : α) :
  ∀a b, tc₁ r a b → r b c → tc₁ r a c :=
begin
  intros a b tab rbc,
  induction tab,
  case tc₁.base: x y rxy ryc {
    exact tc₁.step _ _ _ rxy (tc₁.base _ _ ryc) },
  case tc₁.step: x y z rxy tyz tyc_of_rzc rzc {
    exact tc₁.step _ _ _ rxy (tyc_of_rzc rzc)
  }
end


Question 2

2a

noncomputable def count {α : Type} (a : α) : list α → ℕ
| []        := 0
| (x :: xs) := (if x = a then 1 else 0) + count xs

2b

lemma count_eq_zero_iff_not_mem {α : Type} (a : α) :
  ∀xs, count a xs = 0 ↔ ¬ mem a xs
| []        := by simp [count, mem]
| (x :: xs) :=
  begin
    by_cases x = a;
      simp [count, mem, count_eq_zero_iff_not_mem xs, *],
    rw add_comm,
    apply nat.add_one_ne_zero
  end

2c

lemma count_append {α : Type} (a : α) (ys : list α) :
  ∀xs : list α, count a (xs ++ ys) = count a xs + count a ys
| []        := by simp [count]
| (x :: xs) := by simp [count, count_appendxs]

lemma count_reverse_eq_count {α : Type} (a : α) :
  ∀xs : list α, count a (reverse xs) = count a xs
| []        := by simp [reverse]
| (x :: xs) := by simp [reverse, count, count_append, count_reverse_eq_count xs]


Question 3

3a

instance multiset₁.rel (α : Type) : setoid (list α) :=
{ r     := λxs ys, ∀a, count a xs = count a ys,
  iseqv :=
  ⟨ (assume xs, by simp),
    (assume xs ys ys_xs x, by simp *),
    (assume xs ys zs xs_ys ys_zs, by simp *) ⟩ }

def multiset₁ (α : Type) : Type := quotient (multiset₁.rel α)

3b

def empty_mset₁ {α : Type} : multiset₁ α := ⟦[]⟧

def singleton_mset₁ {α : Type} (a : α) : multiset₁ α := ⟦[a]⟧

def union_mset₁ {α : Type} (A : multiset₁ α) (B : multiset₁ α) : multiset₁ α :=
quotient.lift_on₂ A B (λas bs, ⟦as ++ bs⟧)
  begin
    simp,
    intros as bs as' bs' as_eqv bs_eqv,
    apply quotient.sound,
    intro x,
    simp [count_append, as_eqv x, bs_eqv x]
  end

3c

inductive finite {α : Type} : set α → Prop
| empty : finite ∅
| singleton (a : α) : finite (insert a ∅)
| union (A B : set α) (fin_A : finite A) (fin_B : finite B) : finite (A ∪ B)

def multiset₂ (α : Type) : Type := {f : α → ℕ // finite {x | f x ≠ 0}}

3d

@[simp] lemma compreh_single {α : Type} (a : α) :
  {x : α | ite (x = a) 1 0 ≠ 0} = insert a ∅
:= sorry

@[simp] lemma compreh_union {α : Type} (f g : α → ℕ) :
  {x : α | f x + g x ≠ 0} = {x : α | f x ≠ 0} ∪ {x : α | g x ≠ 0}
:= sorry

def empty_mset₂ {α : Type} : multiset₂ α :=
⟨(λ_, 0), by simp; apply finite.empty⟩

def singleton_mset₂ {α : Type} (a : α) : multiset₂ α :=
⟨(λx, if x = a then 1 else 0), by simp; apply finite.singleton⟩

def union_mset₂ {α : Type} (A B : multiset₂ α) : multiset₂ α :=
⟨(λx, A.1 x + B.1 x),
  begin
    simp,
    apply finite.union,
    apply A.2,
    apply B.2
  end⟩

3e

lemma finite_count_ne_zero {α : Type} (as : list α) :
  finite {x : α | count x as ≠ 0} :=
sorry

def mset₂_of_mset₁ {α : Type} (A : multiset₁ α) : multiset₂ α :=
quotient.lift_on A (λas : list α,
  (subtype.mk (λx, count x as) (finite_count_ne_zero _) : multiset₂ α))
  begin
    intros as as' as_eqv,
    simp,
    apply funext,
    intro x,
    simp [as_eqv x]
  end


Question 4

4a

def wl_of_dl (σ : Type) : dl σ → wl σ
| dl.skip           := wl.skip
| (dl.assign f)     := wl.assign f
| (dl.seq p q)      := wl.seq (wl_of_dl p) (wl_of_dl q)
| (dl.unless p c)   := wl.ite c wl.skip (wl_of_dl p)
| (dl.do_while p c) := wl.seq (wl_of_dl p) (wl.while c (wl_of_dl p))

4b

def dl_of_wl (σ : Type) : wl σ → dl σ
| wl.skip        := dl.skip
| (wl.assign f)  := dl.assign f
| (wl.seq p q)   := dl.seq (dl_of_wl p) (dl_of_wl q)
| (wl.ite c p q) := dl.seq (dl.unless (dl_of_wl p) (λs, ¬ c s)) (dl.unless (dl_of_wl q) c)
| (wl.while c p) := dl.unless (dl.do_while (dl_of_wl p) c) (λs, ¬ c s)

4c

lemma unless_intro (P c : state → Prop) (p : dl state) :
  {* λs, P s ∧ ¬ c s *} p {* P *} → {* P *} dl.unless p c {* P *} :=
sorry

4d

lemma do_while_intro (P Q c : state → Prop) (p : dl state) :
  {* P *} p {* Q *} → {* λs, Q s ∧ c s *} p {* Q *} →
  {* P *} dl.do_while p c {* λs, Q s ∧ ¬ c s *} :=
sorry


Question 5

5a

def den (σ : Type) : ll σ → set (σ × σ)
| ll.skip        := Id σ
| (ll.assign f)  := {st | st.2 = f st.1}
| (ll.seq p q)   := den p ◯ den q
| (ll.ite c p q) := (den p ⇃ c) ∪ (den q ⇃ (λs, ¬ c s))
| (ll.loop p)    := {st | st.1 = st.2 ∨ tc₁ (λs t, (s, t) ∈ den p) st.1 st.2}

5b

def run (σ : Type) : rl σ → σ → σ
| rl.skip               s := s
| (rl.assign f)         s := f s
| (rl.seq p q)          s := run q $ run p s
| (rl.ite c p q)        s := if c s then run p s else run q s
| (rl.repeat 0 _)       s := s
| (rl.repeat (k + 1) p) s := run (rl.repeat k p) $ run p s

5c

The number of constructors of the first argument to `run`, including numbers
in Peano arithmetic.
