documentation exercise questions

Stream: new members

[Sayantan Majumdar]

Its from the induction and recursion chapter

[Sayantan Majumdar]

theorem simp_const_eq (v : ℕ → ℕ) :
∀ e : aexpr, aeval v (simp_const e) = aeval v e :=
sorry

[Kenny Lau]

```
[code goes here]
```

[Kenny Lau]

Please make sure your code can be copied-and-pasted by including the relevant import and/or definitions

[Sayantan Majumdar]

theorem simp_const_eq (v : ℕ → ℕ) :
  ∀ e : aexpr, aeval v (simp_const e) = aeval v e :=
sorry

in the exercise, I am having some trouble making a recursive like proof for (aexpr.plus e1 e2) cases

[Sayantan Majumdar]

inductive aexpr : Type
| const : ℕ → aexpr
| var : ℕ → aexpr
| plus : aexpr → aexpr → aexpr
| times : aexpr → aexpr → aexpr

open aexpr

def aeval (v : ℕ → ℕ) : aexpr → ℕ
| (const n)    := sorry
| (var n)      := v n
| (plus e₁ e₂)  := sorry
| (times e₁ e₂) := sorry

-- BEGIN
def simp_const : aexpr → aexpr
| (plus (const n₁) (const n₂))  := const (n₁ + n₂)
| (times (const n₁) (const n₂)) := const (n₁ * n₂)
| e                             := e

def fuse : aexpr → aexpr := sorry

theorem simp_const_eq (v : ℕ → ℕ) :
  ∀ e : aexpr, aeval v (simp_const e) = aeval v e :=
sorry

theorem fuse_eq (v : ℕ → ℕ) :
  ∀ e : aexpr, aeval v (fuse e) = aeval v e :=
sorry
-- END

[Kenny Lau]

why are there so many sorrys in aeval?

[Sayantan Majumdar]

i am having some trouble with the simp_const_eq

[Sayantan Majumdar]

inductive aexpr : Type
    | const : ℕ → aexpr
    | var : ℕ → aexpr
    | plus : aexpr → aexpr → aexpr
    | times : aexpr → aexpr → aexpr

def aeval (v : ℕ → ℕ) : aexpr → ℕ
    | (aexpr.const n) := n
    | (aexpr.var n) := v n
    | (aexpr.plus e₁ e₂) := (aeval e₁) + (aeval e₂)
    | (aexpr.times e₁ e₂) := (aeval e₁) * (aeval e₂)

    def sample_val : ℕ → ℕ
    | 0 := 5
    | 1 := 6
    | _ := 0

def simple_const : aexpr → aexpr
    | (aexpr.plus (aexpr.const a₁) (aexpr.const a₂)) := aexpr.const (a₁ + a₂)
    | (aexpr.times (aexpr.const a₁) (aexpr.const a₂)) := aexpr.const (a₁ * a₂)
    | e := e

theorem simp_const_eq (v : ℕ → ℕ) : ∀ e : aexpr, aeval v (simple_const e) = aeval v e
    | (aexpr.const a) := rfl
    | (aexpr.var a) := rfl
    -- | (aexpr.plus (aexpr.const n₁) (aexpr.const n₂)) := rfl
    -- | (aexpr.plus (aexpr.const n₁) (aexpr.var n₂)) := rfl
    -- | (aexpr.plus (aexpr.var n₁) (aexpr.const n₂)) := rfl
    -- | (aexpr.plus (aexpr.var n₁) (aexpr.var n₂)) := rfl
    | (aexpr.times e₁ e₂) := sorry

[Sayantan Majumdar]

I hope the formatting is ok now

[Kenny Lau]

since simple_const is not recursively defined, you should be able to do it just like aexpr.plus: by bashing all the cases

[Sayantan Majumdar]

i was hoping there would be a better process

[Kenny Lau]

you can use tactics to help you do the case bashing

[Kenny Lau]

theorem simp_const_eq (v : ℕ → ℕ) : ∀ e : aexpr, aeval v (simple_const e) = aeval v e :=
by intro e; cases e with e e e1 e2 e1 e2; try {refl}; cases e1; cases e2; refl

[Sayantan Majumdar]

thanks