tactic help

Stream: new members

[Jiekai]

inductive AB : Type
| a : AB
| b : AB

def isa (t : AB) : Prop :=
match t with
| AB.a := true
| AB.b := false
end

example : isa AB.a := begin

end

My guess goes to refl and unfold. Both do not work.

[Jiekai]

inductive term : Type
| t : term
| f : term
| ite : term → term → term → term

def is_same_term: term → term → Prop
| term.t      term.t    := true
| term.f      term.f    := true
| (term.ite a1 a2 a3)
  (term.ite b1 b2 b3) :=
    (is_same_term a1 b1) ∧
    (is_same_term a2 b2) ∧
    (is_same_term a3 b3)
| _ _ := false

def v00 := term.t
def v01 := term.f
def v10 := (term.ite term.t v00 v01)

example : is_same_term (term.ite term.t term.t term.f) v10 := begin
/-
simplify tactic failed to simplify
state:
⊢ is_same_term (term.t.ite term.t term.f) v10
-/

  unfold is_same_term,

end

Why is unfold is_same_term not working here?

[Notification Bot]

Jiekai has marked this topic as unresolved.

[Yakov Pechersky]

unfold doesn't see through semireducible definitions. So you have to do:

example : is_same_term (term.ite term.t term.t term.f) v10 :=
begin
  rw v10,
  unfold is_same_term,
  refine ⟨trivial, _, _⟩,
  { rw v00,
    rw is_same_term,
    trivial },
  { rw v01,
    rw is_same_term,
    trivial }
end

[Yakov Pechersky]

I wrote that in long form to be clearer about what's going on.

[Yakov Pechersky]

example : is_same_term (term.ite term.t term.t term.f) v10 :=
by simp [v10, v00, v01, is_same_term]

[Jiekai]

long form appreciated :sweat_smile: