is `apply?` sorryless?

Stream: new members

[Tchsurvives]

I seemed to be able to prove a false statement using `apply?. I was attempting a simple exercise problem in my undergrad course. here's the lean4 code

-- # T1.1.1
-- In this problem we consider binary logical operators in propositional logic.
-- 1. How many are there? (We regard two binary logical operators as the same if they have the same truth table. This question has nothing to do with how many binary logical operators we defined in class.)
-- count the functions from Bool x Bool to Bool
-- if a function is from Bool x Bool to Bool, then it is one of the following
-- f1: (f, f) -> f, (f, t) -> f, (t, f) -> f, (t, t) -> f
def f1 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact false ;
      exact false ;
    cases b2;
      exact false ;
      exact false ;
-- f2: (f, f) -> f, (f, t) -> f, (t, f) -> f, (t, t) -> t
def f2 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact false ;
      exact true ;
    cases b2;
      exact false ;
      exact true ;
-- f3: (f, f) -> f, (f, t) -> f, (t, f) -> t, (t, t) -> f
def f3 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact false ;
      exact false ;
    cases b2;
      exact true ;
      exact false ;
-- f4: (f, f) -> f, (f, t) -> f, (t, f) -> t, (t, t) -> t
def f4 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact false ;
      exact true ;
    cases b2;
      exact true ;
      exact true ;
-- f5: (f, f) -> f, (f, t) -> t, (t, f) -> f, (t, t) -> f
def f5 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact false ;
      exact true ;
    cases b2;
      exact false ;
      exact false ;
-- f6: (f, f) -> f, (f, t) -> t, (t, f) -> f, (t, t) -> t
def f6 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact false ;
      exact true ;
    cases b2;
      exact false ;
      exact true ;
-- f7: (f, f) -> f, (f, t) -> t, (t, f) -> t, (t, t) -> f
def f7 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact false ;
      exact true ;
    cases b2;
      exact true ;
      exact false ;
-- f8: (f, f) -> f, (f, t) -> t, (t, f) -> t, (t, t) -> t
def f8 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact false ;
      exact true ;
    cases b2;
      exact true ;
      exact true ;
-- f9: (f, f) -> t, (f, t) -> f, (t, f) -> f, (t, t) -> f
def f9 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact true ;
      exact false ;
    cases b2;
      exact false ;
      exact false ;
-- f10: (f, f) -> t, (f, t) -> f, (t, f) -> f, (t, t) -> t
def f10 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact true ;
      exact false ;
    cases b2;
      exact false ;
      exact true ;
-- f11: (f, f) -> t, (f, t) -> f, (t, f) -> t, (t, t) -> f
def f11 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact true ;
      exact false ;
    cases b2;
      exact true ;
      exact false ;
-- f12: (f, f) -> t, (f, t) -> f, (t, f) -> t, (t, t) -> t
def f12 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact true ;
      exact false ;
    cases b2;
      exact true ;
      exact true ;
-- f13: (f, f) -> t, (f, t) -> t, (t, f) -> f, (t, t) -> f
def f13 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact true ;
      exact true ;
    cases b2;
      exact false ;
      exact false ;
-- f14: (f, f) -> t, (f, t) -> t, (t, f) -> f, (t, t) -> t
def f14 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact true ;
      exact true ;
    cases b2;
      exact false ;
      exact true ;
-- f15: (f, f) -> t, (f, t) -> t, (t, f) -> t, (t, t) -> f
def f15 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact true ;
      exact true ;
    cases b2;
      exact true ;
      exact false ;
-- f16: (f, f) -> t, (f, t) -> t, (t, f) -> t, (t, t) -> t
def f16 (b1 b2: Bool) : Bool := by
  cases b1;
    cases b2;
      exact true ;
      exact true ;
    cases b2;
      exact true ;
      exact true ;

#eval f5 false false
#eval f5 false true
#eval f5 true false
#eval f5 true true

-- 16 functions
-- define a set of all functions from Bool x Bool to Bool
theorem one_of_16 (f: Bool → Bool → Bool) : f = f1 ∨ f = f2 ∨ f = f3 ∨ f = f4 ∨ f = f5 ∨ f = f6 ∨ f = f7 ∨ f = f8 ∨ f = f9 ∨ f = f10 ∨ f = f11 ∨ f = f12 ∨ f = f13 ∨ f = f14 ∨ f = f15 ∨ f = f16 := by
  cases f (false) (false);
  cases f (false) (true);
  cases f (true) (false);
  cases f (true) (true);
    apply Or.inl; funext b1 b2 ;
      cases b1; cases b2;
        simp [f1] ; apply? ; simp [f1] ; apply? ; simp [f1] ; apply? ;
    apply Or.inr; apply Or.inl; funext b1 b2 ;
      cases b1; cases b2;
        simp [f2] ; apply? ; simp [f2] ; apply? ; simp [f2] ; apply? ;
    apply Or.inr; apply Or.inr; apply Or.inl; funext b1 b2 ;
      cases b1; cases b2;
        simp [f3] ; apply? ; simp [f3] ; apply? ; simp [f3] ; apply? ;
    apply Or.inr; apply Or.inr; apply Or.inr; apply Or.inl; funext b1 b2 ;
      cases b1; cases b2;
        simp [f4] ; apply? ; simp [f4] ; apply? ; simp [f4] ; apply? ;
    apply Or.inr; apply Or.inr; apply Or.inr; apply Or.inr; apply Or.inl;
      -- let meow := f false false
    funext b1 b2 ;
      cases b1; cases b2;
        simp [f5] ;  -- WEIRD this line is weird
        apply? ; simp [f5] ; apply? ; simp [f5] ; apply? ;

the line with -- WEIRD comment is the misbehaving line, where I proved that f (false) (false) = false when it should be true

[Tchsurvives]

if there's any more efficient way to enumerate all binary logical operators i would be keen to learn about it too!

[Tchsurvives]

i narrowed it down to a slimmer example

theorem wonky (f: Unit → Bool) : (f = λ _ => false) ∨ (f = λ _ => true) := by
  cases f () with
  | false => apply Or.inr; funext _; apply?;
  | true => apply Or.inr; funext _; apply?;

#check wonky

[Tchsurvives]

nvm i just learned it does indeed contain sorry, thanks @Clarence Chew for the help

theorem wonky (f: Unit → Bool) : (f = λ _ => false) ∨ (f = λ _ => true) := by
  cases t: f ();
  apply Or.inl; funext _; exact t;
  apply Or.inr; funext _; exact t;

#check wonky

[Kyle Miller]

It looks like apply? isn't able to solve the goal itself (it gives a long list of suggestions for how you might make progress, but notice all of them have a ?metavariable for a goal you will have to fill in yourself).