nat/bool expression language

Stream: new members

[Luisa Cicolini]

I am trying to solve the exercises from "Types and Programming Languages" by B. Pierce in Lean and am currently stuck on the proof of exercise 3.5.14.

The objective is to prove that given a type:

inductive t' where
  | True : t'
  | False : t'
  | ite : t' → t' → t' → t'
  | zero : t'
  | succ : t' → t'
  | pred : t' → t'
  | iszero : t' → t'

and defining evaluation as:

inductive t'.EvaluatesTo : t' → t' → Prop
| -- ite true t₂ t₃ → t₂
  EvaluatesToTrue: t'.EvaluatesTo (t'.True.ite t₂ t₃) t₂
| -- ite false t₂ t₃ → t₃
  EvaluatesToFalse: t'.EvaluatesTo (t'.False.ite t₂ t₃) t₃
| -- (c → c') → (ite c l r → ite c' l r)
  EvaluatesToIf (h : t'.EvaluatesTo c c') : (c.ite l r).EvaluatesTo (c'.ite l r)
| -- (t₁ → t₁') → (succ t₁ → succ t₂)
  EvaluatesToSucc (h : t'.EvaluatesTo t₁ t₁') : (t'.succ t₁).EvaluatesTo (t'.succ t₁')
| -- pred 0 = 0
  EvaluatesToZero : (t'.pred t'.zero).EvaluatesTo (t'.zero)
| -- pred (succ nv) → nv
  EvaluatesToPredSucc : (t'.pred (t'.succ t₁)).EvaluatesTo  (t₁)
| -- (t₁ → t₁') → (pred t₁ → pred t₂)
  EvaluatesToPred (h : t'.EvaluatesTo t₁ t₁') : (t'.pred t₁).EvaluatesTo (t'.pred t₁')
| -- iszero 0 → true
  EvaluatesToIsZeroZero : (t'.iszero t'.zero).EvaluatesTo (t'.True)
| -- iszero (succ nv) → false
  EvaluatesToIsZeroSucc : (t'.iszero (t'.succ _)).EvaluatesTo (t'.False)
| -- (t₁ → t₁') → (iszero t₁ → iszero t₂)
  EvaluatesToIsZero (h : t'.EvaluatesTo t₁ t₁') : (t'.iszero t₁).EvaluatesTo (t'.iszero t₁')

the following theorem holds:

theorem OneStepDeterminacy' (a b c : t') (hab : t'.EvaluatesTo a b) (hac : t'.EvaluatesTo a c) : b = c := by sorry

I am proving this by induction on a and keep getting stuck in the case where a is of the form pred s:

ih : ∀ (b c : t'), s.EvaluatesTo b → s.EvaluatesTo c → b = c
⊢ ∀ (b c : t'), s.pred.EvaluatesTo b → s.pred.EvaluatesTo c → b = c

in particular, I've tried doing various cases, induction on s and on the evaluation rules, but I don't see how to lay out the overall proof strategy for this case.

[Shreyas Srinivas]

Hi, it would be much easier for us to help you if you gave us an #mwe

[pandaman]

I think the theorem is false?

def t : t' := .pred (.succ (.pred .zero))

-- different one step evaluation!
theorem ev₁ : t.EvaluatesTo (.pred .zero) := .EvaluatesToPredSucc
theorem ev₂ : t.EvaluatesTo (.pred (.succ .zero)) := .EvaluatesToPred (.EvaluatesToSucc .EvaluatesToZero)

In general (if the relation is fixed), you want to induct on the EvaluatesTo relation with generalizing c. This gives us an induction hypothesis with variable c, which we can use to match the shape of the terms in each branch. In each branch, cases hac will eliminate most cases thanks to Lean's dependent pattern matching, but you'll need a few manual analysis to eliminate the remaining cases.

[Luisa Cicolini]

oh I see, I had not realized that. I guess I need to reconsider the encodings. Thank you very much!
(mwe here with the sorrys where I gost stuck)

[Luisa Cicolini]

thanks for the catch @pandaman, I've asked a more precise question here with all the references to the book :)
do you think I've missed something in the encoding? Or is the exercise just wrong?
EDIT: turns out encoding nats and bools in the same type was the problem.

[pandaman]

An option is to define an IsNumericValue : t' -> Prop inductive predicate and use it as a precondition of the evaluation relation.

[Luisa Cicolini]

I think I fixed the definitions now, but I still get stuck in the same proof. A mwe is here, could anyone help me out with the sorrys? In particular, I get stuck with the cases on the hypothesis and tried induction b with no success

[pandaman]

Here is my attempt to prove the theorem

inductive t' where
  | True : t'
  | False : t'
  | ite : t' → t' → t' → t'
  | zero : t'
  | succ : t' → t'
  | pred : t' → t'
  | iszero : t' → t'
  deriving Repr

inductive nv : t' → Prop where
  | zero : nv t'.zero
  | succ n : nv n → nv (t'.succ n)

inductive t'.EvaluatesTo : t' → t' → Prop
| -- ite true t₂ t₃ → t₂
  EvaluatesToTrue {t₁ t₁' : t'} : t'.EvaluatesTo (True.ite t₁ t₁') t₁
| -- ite false t₂ t₃ → t₃
  EvaluatesToFalse {t₁ t₁' : t'} : t'.EvaluatesTo (False.ite t₁ t₁') t₁'
| -- (c → c') → (ite c l r → ite c' l r)
  EvaluatesToIf {t₁ t₁' : t'} (h : t'.EvaluatesTo c c') : t'.EvaluatesTo (c.ite l r) (c'.ite l r)
| -- (t₁ → t₁') → (succ t₁ → succ t₂)
  EvaluatesToSucc {t₁ t₁' : t'} (h : EvaluatesTo t₁ t₁') : (EvaluatesTo (t'.succ t₁) (t'.succ t₁'))
| -- pred 0 = 0
  EvaluatesToZero : t'.EvaluatesTo (t'.pred t'.zero) (t'.zero)
| -- pred (succ nv) → nv
  EvaluatesToPredSucc (h : nv v₁) : t'.EvaluatesTo (t'.pred (t'.succ v₁))  (v₁)
| -- (t₁ → t₁') → (pred t₁ → pred t₂)
  EvaluatesToPred (h : t'.EvaluatesTo t₁ t₁') : t'.EvaluatesTo (t'.pred t₁) (t'.pred t₁')
| -- iszero 0 → true
  EvaluatesToIsZeroZero : t'.EvaluatesTo (t'.iszero t'.zero) (t'.True)
| -- iszero (succ nv) → false
  EvaluatesToIsZeroSucc (h : nv v₁) : t'.EvaluatesTo (t'.iszero (t'.succ v₁)) (t'.False)
| -- (t₁ → t₁') → (iszero t₁ → iszero t₂)
  EvaluatesToIsZero (h : t'.EvaluatesTo t₁ t₁') : t'.EvaluatesTo (t'.iszero t₁) (t'.iszero t₁')

/-
It's helpful to prove so-called "inversion" lemmas for the inductive rules first.

In general, inversion lemmas state that "if an evaluation of this form holds, then there must be something
that makes the evaluation hold". In this case, we only need inversion lemmas that state "there cannot be
an evaluation of this form", like evaluating from `True` or `False`.
-/
theorem true_no_step (t : t') : ¬t'.EvaluatesTo t'.True t := by
  intro h
  -- Lean detects that no `EvaluatesTo` rule can apply for `True`.
  cases h

theorem false_no_step (t : t') : ¬t'.EvaluatesTo t'.False t := by
  intro h
  -- Lean detects that no `EvaluatesTo` rule can apply for `False`.
  cases h

theorem zero_no_step (t : t') : ¬t'.EvaluatesTo t'.zero t := by
  intro h
  -- Lean detects that no `EvaluatesTo` rule can apply for `zero`.
  cases h

-- A numeric value is a value (i.e., no evaluation from it)
theorem nv_no_step (v t : t') (n : nv v) : ¬t'.EvaluatesTo v t := by
  induction n generalizing t with
  | zero => exact zero_no_step t
  | succ v n ih =>
    intro h'
    cases h' with
    | EvaluatesToSucc h'' => exact absurd h'' (ih _)

/-- exercise 3.5.14: show that theorem 3.5.4 also holds for t' -/
theorem OneStepDeterminacy' (a b c : t') (hab : t'.EvaluatesTo a b) (hac : t'.EvaluatesTo a c) : b = c := by
  induction hab generalizing c with
  | @EvaluatesToTrue t₁ t₁' =>
    cases hac with
    | EvaluatesToTrue => rfl
    -- A hole (`_`) lets Lean find the appropriate argument for `true_no_step`. We can use a hole here
    -- since the necessary information (the term after one step) is already present in `h`.
    | EvaluatesToIf h => exact absurd h (true_no_step _)
  | EvaluatesToFalse =>
    cases hac with
    | EvaluatesToFalse => rfl
    | EvaluatesToIf h => exact absurd h (false_no_step _)
  -- `@` allows us to match on the implicit arguments
  | @EvaluatesToIf cond₁ cond₁' l r t₁ t₁' h ih =>
    cases hac with
    | EvaluatesToTrue => exact absurd h (true_no_step _)
    | EvaluatesToFalse => exact absurd h (false_no_step _)
    | @EvaluatesToIf cond₂ cond₂' l r t₂ t₂' h' =>
      have eq : cond₁' = cond₂' := ih cond₂' h'
      rw [eq]
  | @EvaluatesToSucc t₁ t₁' h₁ ih =>
    cases hac with
    | @EvaluatesToSucc t₂ t₂' h₂ =>
      have eq : t₁' = t₂' := ih t₂' h₂
      rw [eq]
  | EvaluatesToZero =>
    cases hac with
    | EvaluatesToZero => rfl
    | @EvaluatesToPred t₂ t₂' h₂ => exact absurd h₂ (zero_no_step _)
  | @EvaluatesToPredSucc v₁ n₁ =>
    cases hac with
    | EvaluatesToPredSucc => rfl
    | @EvaluatesToPred t₂ t₂' h₂ =>
      have n₁' : nv (t'.succ v₁) := nv.succ v₁ n₁
      exact absurd h₂ (nv_no_step _ _ n₁')
  | @EvaluatesToPred t₁ t₁' h₁ ih =>
    cases hac with
    | EvaluatesToZero => exact absurd h₁ (zero_no_step _)
    | EvaluatesToPredSucc n =>
      have n' : nv (t'.succ c) := nv.succ c n
      exact absurd h₁ (nv_no_step _ _ n')
    | @EvaluatesToPred t₂ t₂' h₂ =>
      have eq : t₁' = t₂' := ih t₂' h₂
      rw [eq]
  | EvaluatesToIsZeroZero =>
    cases hac with
    | EvaluatesToIsZeroZero => rfl
    | @EvaluatesToIsZero t₂ t₂' h₂ => exact absurd h₂ (zero_no_step _)
  | @EvaluatesToIsZeroSucc v₁ n₁ =>
    cases hac with
    | EvaluatesToIsZeroSucc => rfl
    | @EvaluatesToIsZero t₂ t₂' h₂ =>
      have n₁' : nv (t'.succ v₁) := nv.succ v₁ n₁
      exact absurd h₂ (nv_no_step _ _ n₁')
  | @EvaluatesToIsZero t₁ t₁' h₁ ih =>
    cases hac with
    | EvaluatesToIsZeroZero => exact absurd h₁ (zero_no_step _)
    | @EvaluatesToIsZeroSucc v₂ n₂ =>
      have n₂' : nv (t'.succ v₂) := nv.succ v₂ n₂
      exact absurd h₁ (nv_no_step _ _ n₂')
    | @EvaluatesToIsZero t₂ t₂' h₂ =>
      have eq : t₁' = t₂' := ih t₂' h₂
      rw [eq]

[pandaman]

Since we are interested in the evaluation, it's generally more easier to perform induction on the EvaluatesTo inductive predicate(i.e., the induction over the structure of how an EvaluatesTo derivation is constructed). Induction over the inductive predicate gives you more context about how the evaluation should behave.

[Luisa Cicolini]

thank you very much @pandaman! That makes a lot of sense. I guess I was trying to follow the on-paper proof strategy the book suggests, but it's clearly very different than doing it in Lean.

[pandaman]

I think TAPL also suggests using induction over the derivation when proving (3.5.4), the original version without additional rules. Anyway, what's missing in your version is probably the lemma that states a numeric value cannot be evaluated further (nv_no_step in my example).

[pandaman]

Otherwise, I think your version is very close to the final proof. Good luck!

[Luisa Cicolini]

Thanks again!! That is all very helpful :)

[Luisa Cicolini]

It all worked and is now much clearer to me how the proof strategy works :)