splitting decidable (a /\ b \/ c /\ ...)

Stream: general

[Hunter Freyer]

If my goal is something like decidable (a /\ (b \/ c) /\ ...), how can I quickly split that into separate goals for decidable a and decidable b \/ c, etc?

[Kevin Buzzard]

Try decidable_and? No idea if it's there but that's what I'd call it

[Simon Hudon]

Because decidable is a type class, we can find many definitions with that type using #print instances:

#print instances decidable
-- xor.decidable : Π {p q : Prop} [_inst_1 : decidable p] [_inst_2 : decidable q], decidable (xor p q)
-- iff.decidable : Π {p q : Prop} [_inst_1 : decidable p] [_inst_2 : decidable q], decidable (p ↔ q)
-- implies.decidable : Π {p q : Prop} [_inst_1 : decidable p] [_inst_2 : decidable q], decidable (p → q)
-- not.decidable : Π {p : Prop} [_inst_1 : decidable p], decidable (¬p)
-- or.decidable : Π {p q : Prop} [_inst_1 : decidable p] [_inst_2 : decidable q], decidable (p ∨ q)
-- and.decidable : Π {p q : Prop} [_inst_1 : decidable p] [_inst_2 : decidable q], decidable (p ∧ q)
-- decidable.false : decidable false
-- decidable.true : decidable true

This tells us that and.decidable is what you're looking for

[Hunter Freyer]

@Simon Hudon I would have thought that, but it doesn't work:

theorem foo : Π (a b : Prop), decidable (a ∧ b) := begin
    intros,
    apply and.decidable, -- "failed to synthesize type class instance"
end

[Hunter Freyer]

This post from 2017 seems to indicate that you can't use decidable like that because it's a type class, not a normal predicate? But that may be outdated and/or incorrect

[Simon Hudon]

You can use it like this:

theorem foo : Π (a b : Prop), decidable (a ∧ b) :=
begin
    intros,
    have h₀ : decidable a, sorry,
    have h₁ : decidable b, sorry,
    resetI,
    apply_instance,
end

[Simon Hudon]

resetI will add h₀ and h₁ to the instance cache

[Reid Barton]

decidable is a type class and meant to be used in type class-y ways. What are you really trying to do?

[Reid Barton]

Normally you shouldn't end up with decidable goals at all

[Reid Barton]

Either use classical or write the instances you need

[Mario Carneiro]

One trick I sometimes use when I want lean to not infer a typeclass is refine @and.decidable _ _ (id _) (id _)

[Mario Carneiro]

It seems like a mistake that lean will infer instances even if you write @foo ... _, but I can see that many things will break if this changes. It would be nice if there was a mode that allowed this to be "no really" explicit

[Reid Barton]

Lean 4 has a distinction between _ and ? (I think that's the syntax), which maybe would apply here too

[Reid Barton]

with one meaning "infer" and the other meaning "make a new goal"

[Hunter Freyer]

@Reid Barton I'm trying to show a predicate is decidable... What should the goal be, if not "decidable"?

[Mario Carneiro]

If so you are writing a program and probably shouldn't be using tactics until you get to the proof part

[Reid Barton]

then normally the proof would be some variant of by { dunfold [...], apply_instance } or use decidable_of_iff

[Mario Carneiro]

But if your predicate has lots of ands and ors in it you should probably be doing what Simon showed. Assuming by apply_instance alone doesn't work, add the necessary instances to the context with haveI and then use apply_instance

[Mario Carneiro]

this mostly only comes up for recursive predicates. For nonrecursive predicates Reid's suggestion is the best

[Hunter Freyer]

Here's what I'm working with:

@[derive decidable_eq]
inductive val : Type
| nat
| nil
| cons : Π (car : val) (cdr: val), val

@[derive decidable_eq]
inductive fn2 : Type
| zero : fn2
| succ : fn2
| car  : fn2
| cdr  : fn2
| nil  : fn2
| cons (car cdr : fn2) : fn2
| comp (f g : fn2) : fn2
| prec (z_case s_case : fn2) : fn2

inductive typed : fn2 -> val -> val -> Prop
| zero : typed fn2.zero val.nil val.nat
| succ : typed fn2.succ val.nat val.nat
| car {tcar tcdr : val} : typed fn2.car (val.cons tcar tcdr) tcar
| cdr {tcar tcdr : val} : typed fn2.cdr (val.cons tcar tcdr) tcdr
| nil {t: val} : typed fn2.nil t val.nil
| cons {tin tcar tcdr: val} {car cdr : fn2}
    (tcar_t : typed car tin tcar)
    (tcdr_t : typed cdr tin tcdr) :
    typed (fn2.cons car cdr) tin (val.cons tcar tcdr)
| comp {tin tint tout: val} {f g : fn2}
    (f_t : typed f tint tout)
    (g_t : typed g tin tint) :
    typed (fn2.comp f g) tin tout
| prec {trest tout: val} {z_case s_case : fn2}
    (z_t : typed z_case trest tout)
    (s_t : typed s_case (val.cons val.nat (val.cons tout trest)) tout):
    typed (fn2.prec z_case s_case) (val.cons val.nat trest) tout

mk_iff_of_inductive_prop typed typed_iff

@[instance] def typed.decidable (f : fn2) (tin tout : val) : decidable (typed f tin tout) :=
begin

[Hunter Freyer]

Trying to show that whether a type assignment is correct or not is decidable.

[Mario Carneiro]

The top level should be a recursion using the equation compiler

[Hunter Freyer]

writing it out in a forward way will work, but it's so duplicative of the definition of typed that it seems like metaprogramming should surely be better, right? I guess not if you say so

[Mario Carneiro]

Eh, actually some of this is a bit annoying, metaprogramming is better

[Hunter Freyer]

I don't actually know how to prove false in the cases that don't match any constructor.

[Mario Carneiro]

actually it is better to phrase this as a function from fn to its type

[Mario Carneiro]

def fn2.typecheck : fn2 → val → option val
| fn2.zero val.nil := some val.nat
| fn2.succ val.nat := some val.nat
| fn2.car (val.cons tcar tcdr) := some tcar
| fn2.cdr (val.cons tcar tcdr) := some tcdr
| fn2.nil _ := some val.nil
| (fn2.cons car cdr) tin := do
  tcar ← car.typecheck tin,
  tcdr ← cdr.typecheck tin,
  return (val.cons tcar tcdr)
| (fn2.comp f g) tin := do
  tint ← g.typecheck tin,
  f.typecheck tint
| (fn2.prec z_case s_case) (val.cons val.nat trest) := do
  tout ← z_case.typecheck trest,
  tout' ← s_case.typecheck (val.cons val.nat (val.cons tout trest)),
  guard (tout' = tout),
  return tout
| _ _ := none

theorem fn2.typecheck_iff {f : fn2} {tin tout : val} :
  typed f tin tout ↔ f.typecheck tin = some tout :=
sorry

instance typed.decidable (f : fn2) (tin tout : val) : decidable (typed f tin tout) :=
decidable_of_iff' _ fn2.typecheck_iff

[Mario Carneiro]

theorem fn2.typecheck_iff {f : fn2} {tin tout : val} :
  typed f tin tout ↔ f.typecheck tin = some tout :=
begin
  split,
  { intro h, induction h; try {refl};
    simp [fn2.typecheck, *, return, pure] },
  { induction f generalizing tin tout,
    iterate 5 {{ cases tin; rw typed_iff; simp [fn2.typecheck, eq_comm] }},
    { simp [fn2.typecheck],
      rintro a h1 b h2 ⟨⟩,
      constructor; solve_by_elim },
    { simp [fn2.typecheck],
      rintro a h1 h2,
      constructor; solve_by_elim },
    { cases tin with car trest; try { simp [fn2.typecheck] },
      cases car; simp [fn2.typecheck],
      rintro a h1 b h2 ⟨⟩ ⟨⟩,
      constructor; solve_by_elim } }
end

[Mario Carneiro]

@Hunter Freyer