error for theorem, expects function

Stream: lean4

[Jared green]

at lines 214 and 228

import Init.Data.List
import Std.Data.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic

open Classical

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred
deriving DecidableEq

namespace normalizable

@[reducible]
def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

@[simp]
theorem toProp_not : toProp (Not n₁) ↔ ¬ toProp n₁ := Iff.rfl

@[simp]
theorem toProp_and : toProp (And n₁ n₂) ↔ toProp n₁ ∧ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_or : toProp (Or n₁ n₂) ↔ toProp n₁ ∨ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_atom {a : α} : toProp (atom a : normalizable α pred) ↔ pred a := Iff.rfl


def subnormalize (n : (normalizable α pred)) : List (List (List (normalizable α pred))) :=
  match n with
  | Or a b => [[a,n],[b,n],[Not a,Not b, Not n]] :: (List.append (subnormalize a) (subnormalize b))
  | And a b => [[a,b,n],[Not a,Not n],[Not b,Not n]] :: (List.append (subnormalize a) (subnormalize b))
  | Not i => [[n,Not i],[Not n, i]] :: (subnormalize i)
  | atom _ => [[[n],[Not n]]]

def normalize :  normalizable α pred -> List (List (List (normalizable α pred))) := fun o =>
  [[o]] :: (subnormalize o)

def nStrip (n : normalizable α pred) : Bool × normalizable α pred :=
  match n with
  | Not i => (false,i)
  | i => (true,i)

def booleanize (n : List (List (List (normalizable α pred)))) : List (List (List (Bool × normalizable α pred))) :=
  n.map (fun x => x.map (fun y => y.map (fun z => nStrip z)))

def normalizel (n : normalizable α pred) : List (List (List (Bool × normalizable α pred))) :=
  booleanize (normalize n)

def wToProp (w : Bool × normalizable α pred) : Prop :=
  if w.fst then toProp w.snd else ¬(toProp w.snd)

def sToProp (s : List (Bool × normalizable α pred)) : Prop :=
  s.all (fun x => wToProp x)

def gToProp (g : List (List (Bool × normalizable α pred))) : Prop :=
  g.any (fun x => sToProp x)

def nToProp (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
  n.all (fun x => gToProp x)

def fToProp (n : List (List (List (normalizable α pred)))) : Prop :=
  n.all (fun x => x.any (fun y => y.all (fun z => toProp z)))

theorem nStrip_equiv : ∀ n : normalizable α pred, toProp n <-> wToProp (nStrip n) :=
  by
  intro n
  unfold nStrip
  induction n
  simp
  unfold wToProp
  simp
  simp
  unfold wToProp
  simp
  unfold wToProp
  simp
  simp
  unfold wToProp
  simp

theorem booleanize_eqiv : ∀ n : List (List (List (normalizable α pred))), fToProp n <-> nToProp (booleanize n) :=
  by
  intro n
  unfold nToProp
  simp
  unfold fToProp
  simp
  unfold booleanize
  simp
  unfold gToProp
  simp
  unfold sToProp
  simp
  simp [nStrip_equiv]

theorem andGateTaut : (¬ a ∧ ¬(a ∧ b)) ∨ (¬ b ∧ ¬(a ∧ b)) ∨ (a ∧ b ∧ (a ∧ b)) :=
  by
  cases Classical.em a
  cases Classical.em b
  right
  right
  constructor
  assumption
  constructor
  assumption
  constructor
  assumption
  assumption
  right
  left
  constructor
  assumption
  push_neg
  intro
  assumption
  left
  constructor
  assumption
  rw [and_comm]
  push_neg
  intro
  assumption

theorem orGateTaut : (a ∧ (a ∨ b)) ∨ (b ∧ (a ∨ b)) ∨ ((¬ a) ∧ (¬b) ∧ ¬(a ∨ b)) = true :=
  by
  simp
  cases Classical.em a
  left
  constructor
  assumption
  left
  assumption
  right
  cases Classical.em b
  left
  constructor
  assumption
  right
  assumption
  right
  constructor
  assumption
  constructor
  assumption
  push_neg
  constructor
  assumption
  assumption

theorem all_and : List.all ( a ++ b) c <-> List.all a c ∧ List.all b c :=
  by
  simp
  constructor
  intro ha
  constructor
  intro b
  intro hb
  apply ha
  left
  exact hb
  intro c
  intro hc
  apply ha
  right
  exact hc
  intro ha
  intro b
  intro hb
  cases hb
  apply ha.left
  assumption
  apply ha.right
  assumption

theorem subnormal : ∀ n : normalizable α pred, fToProp (subnormalize n) :=
  by
  intro n
  induction' n with a b c d e f g i j k l
  unfold subnormalize
  unfold fToProp
  simp
  unfold toProp
  apply Classical.em
  unfold subnormalize
  simp
  unfold fToProp
  rw [List.all_cons]
  simp only [List.any_cons, List.all_cons, List.all_nil, Bool.and_true, List.any_nil,
    Bool.or_false, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq,
    List.mem_append, List.any_eq_true]
  constructor
  rw [toProp_not]
  rw [toProp_and]
  exact andGateTaut (toProp b) (toProp c) --function expected...
  rw [all_and]
  constructor
  assumption
  assumption
  unfold fToProp
  unfold subnormalize
  rw [List.all_cons]
  simp only [List.any_cons, List.all_cons, toProp_or, List.all_nil, Bool.and_true, toProp_not,
    List.any_nil, Bool.or_false, List.append_eq, Bool.and_eq_true, Bool.or_eq_true,
    decide_eq_true_eq, List.mem_append, List.any_eq_true]
  constructor
  rw [toProp_not]
  rw [toProp_or]
  exact orGateTaut (toProp f) (toProp g) --function expected...
  rw [all_and]
  constructor
  assumption
  assumption
  unfold fToProp
  unfold subnormalize
  rw [List.all_cons]
  simp only [List.any_cons, List.all_cons, toProp_not, List.all_nil, Bool.and_true, Bool.and_self,
    not_not, List.any_nil, Bool.or_false, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq,
     List.any_eq_true]
  constructor
  cases Classical.em (toProp k)
  right
  assumption
  left
  assumption
  unfold fToProp at l
  exact l

[Kevin Buzzard]

normalizable.andGateTaut {a b : Prop} : ¬a ∧ ¬(a ∧ b) ∨ ¬b ∧ ¬(a ∧ b) ∨ a ∧ b ∧ a ∧ b. Do you understand what the {a b : Prop} brackets mean? Take a look at the "implicit arguments" section in Chapter 2 of #tpil

[Jared green]

placing underscores gets the same message.

[Jared green]

it does close the goal, so i wonder if the messages can be ignored.

[Kevin Buzzard]

Did you take a look at the section I mentioned above yet?

[Kevin Buzzard]

You can never ignore errors btw. Any message (such as "no goals") after an error is meaningless.

[Jared green]

i read it.

[Kevin Buzzard]

So you understand the error now?

[Jared green]

no

[Kevin Buzzard]

Your definition of andGateTaut makes the inputs implicit. You are attempting to give them explicitly.

[Jared green]

what should the line look like?

[Jared green]

not giving them results in a type mismatch.

[Kevin Buzzard]

Well you have two choices. Either you change the definition of andGateTaut to make the inputs explicit, or you don't give the inputs at all and hope that lean can infer them.

[Kevin Buzzard]

Oh there's a third choice: you use the (a := toProp b) syntax

[Kevin Buzzard]

To better understand what's going on, I recommend that you set_option autoImplicit false and also the other one whose name I don't remember -- something like set_option weakAutoImplicit false. These are options which default to true but I have a mountain of evidence that they're very confusing for beginners. Once you do this your code will break because all the times you've used a variable without declaring it you'll now get an error, forcing you to add lines like variable (a : Prop). When you add these lines you'll be forced to think about brackets, and this will help you understand what's going on

[Kevin Buzzard]

Jared green said:

not giving them results in a type mismatch.

This probably means that your proof is incorrect.

  exact andGateTaut (a := toProp b) (b := toProp c)

(which is my understanding of what you're trying to say) gives the error

type mismatch
  andGateTaut
has type
  ¬toProp b ∧ ¬(toProp b ∧ toProp c) ∨
    ¬toProp c ∧ ¬(toProp b ∧ toProp c) ∨ toProp b ∧ toProp c ∧ toProp b ∧ toProp c : Prop
but is expected to have type
  toProp b ∧ toProp c ∧ toProp b ∧ toProp c ∨
    ¬toProp b ∧ toProp (Not (And b c)) ∨ toProp (Not c) ∧ toProp (Not (And b c)) : Prop

so as well as your issue with implicit/explicit functions, you have this problem too (in fact my impression is that this is your main problem).

[Jared green]

so it turns out clause order matters... problem solved.

[Damiano Testa]

Jared green said:

it does close the goal, so i wonder if the messages can be ignored.

Kevin Buzzard said:

You can never ignore errors btw. Any message (such as "no goals") after an error is meaningless.

When lean encounters an error, it liberally introduces sorry for the sake of "let's try to keep parsing this". This does mean that you can sometimes catch more than one error. However, any type checking claim (e.g. No goals) is meaningless.