proof using and_assoc.mp

Stream: new members

[Daniel Bush]

This is an exercise in the logic game at https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic/world/IffIntro/level/6 .

It can be solved by rewriting the goal to match h:

example (P Q R : Prop) (h : (P ∨ Q ∨ R) → ¬(P ∧ Q ∧ R)) : ((P ∨ Q) ∨ R) → ¬((P ∧ Q) ∧ R) := by
  rw [or_assoc, and_assoc]
  exact h

But another way is suggested, starting with imp_trans (transitive implication), which I created as

theorem imp_trans {A B C : Prop} (h1 : A → B) (h2 : B → C) : A → C :=
  h2 ∘ h1

and then doing something like:

example (P Q R : Prop) (h : (P ∨ Q ∨ R) → ¬(P ∧ Q ∧ R)) : ((P ∨ Q) ∨ R) → ¬((P ∧ Q) ∧ R) :=
  have h2 := (imp_trans and_assoc.mp)
  have h1 := (imp_trans or_assoc.mp h)
  have h3 := imp_trans h1 h2
  show ((P ∨ Q) ∨ R) → ¬((P ∧ Q) ∧ R)  from h3

The above could be more succinct, but I've broken it up. The problem I'm having is what is lean doing with h2 for the line: have h2 := (imp_trans and_assoc.mp)...

• (1) h1's input is the input for or_assoc.mp which is a function that takes evidence for (P ∨ Q) ∨ R and returns something of type P ∨ Q ∨ R which then feeds into h which then outputs something of type ¬(P ∧ Q ∧ R) (that seems pretty straight forward)
• (2) Lean type checks h2 as (P ∧ Q ∧ R → False) → (P ∧ Q) ∧ R → False which I interpet as (P ∧ Q ∧ R → False) → ((P ∧ Q) ∧ R → False) - which solves the problem...
• But how do we get this type from imp_trans and_assoc.mp? I thought and_assoc.mp is taking evidence for (P ∧ Q) ∧ R and returning something of type P ∧ Q ∧ R?

[Richard Copley]

Look at the types of h2 and h1 by putting the cursor on the sorry below.

theorem imp_trans {A B C : Prop} (h1 : A → B) (h2 : B → C) : A → C :=
  h2 ∘ h1

example (P Q R : Prop) (h : (P ∨ Q ∨ R) → ¬(P ∧ Q ∧ R)) : ((P ∨ Q) ∨ R) → ¬((P ∧ Q) ∧ R) :=
  have h2 := (imp_trans and_assoc.mp)
  have h1 := imp_trans or_assoc.mp h
  sorry

The types of the arguments are unknown at this point and are represented as metavariables (in this case, as unknown functions of the stuff in scope, namely P, Q, R and h). When you add the have h3 line, you give Lean enough information to deduce what values those metavariables must have.

But how do we get this type from imp_trans and_assoc.mp? I thought and_assoc.mp is taking evidence for (P ∧ Q) ∧ R and returning something of type P ∧ Q ∧ R?

It's hard to know exactly where the difficulty is. Sorry! Yes, that is what and_assoc.mp does, and that's what you need here, so the proof goes through.

• Are you bearing in mind that ¬x is defined as x → False?
• Stepping through "term-mode" proofs is quite confusing. Is it any clearer if you instead inspect this slightly expanded "tactic-mode" proof?

theorem imp_trans {A B C : Prop} (h1 : A → B) (h2 : B → C) : A → C :=
  h2 ∘ h1

example (P Q R : Prop) (h : (P ∨ Q ∨ R) → ¬(P ∧ Q ∧ R)) : ((P ∨ Q) ∨ R) → ¬((P ∧ Q) ∧ R) := by
  have h4 := and_assoc.mp
  have h2 := imp_trans h4
  have h1 := imp_trans or_assoc.mp h
  have h3 := imp_trans h1 h2
  exact h3

[Daniel Bush]

Thanks for replying Richard.

Richard Copley said:

Look at the types of h2 and h1 by putting the cursor on the sorry below.

theorem imp_trans {A B C : Prop} (h1 : A → B) (h2 : B → C) : A → C :=
  h2 ∘ h1

example (P Q R : Prop) (h : (P ∨ Q ∨ R) → ¬(P ∧ Q ∧ R)) : ((P ∨ Q) ∨ R) → ¬((P ∧ Q) ∧ R) :=
  have h2 := (imp_trans and_assoc.mp)
  have h1 := imp_trans or_assoc.mp h
  sorry

The types of the arguments are unknown at this point and are represented as metavariables (in this case, as unknown functions of the stuff in scope, namely P, Q, R and h). When you add the have h3 line, you give Lean enough information to deduce what values those metavariables must have.

But how do we get this type from imp_trans and_assoc.mp? I thought and_assoc.mp is taking evidence for (P ∧ Q) ∧ R and returning something of type P ∧ Q ∧ R?

It's hard to know exactly where the difficulty is. Sorry! Yes, that is what and_assoc.mp does, and that's what you need here, so the proof goes through.

• Are you bearing in mind that ¬x is defined as x → False?
• Stepping through "term-mode" proofs is quite confusing. Is it any clearer if you instead inspect this slightly expanded "tactic-mode" proof?
  

Maybe I can come at this from what lean is doing.

Lean is doing this from the original example:

• h1: (P ∨ Q) ∨ R → ¬(P ∧ Q ∧ R)
• h2: (P ∧ Q ∧ R → False) → (P ∧ Q) ∧ R → False
• h3: (P ∨ Q) ∨ R → (P ∧ Q) ∧ R → False

I can mark out initial and final output types, so as to focus on the bit that's left that I don't get:

• h1: inital_input_type → (P ∧ Q ∧ R) -> False
• h2: (P ∧ Q ∧ R → False) → final_output_type
• h3: initial_input_type → final_output_type

It's clear h1 and h2 will chain together under imp_trans in h3.

h1 I think I understand: or_assoc.mp h takes a value of type (P ∨ Q) ∨ R and converts it to P ∨ Q ∨ R by or_assoc.mp and then converts it to (P ∧ Q ∧ R) -> False by h.

But I cannot see what the conversions are using and_assoc.mp in h2.

Where is and_assoc.mp called within h2? What other function(s) are called before or after it as part of h2, and what are their types? Or in other words: Can we state what the sequence of type conversions are in a sentence like I did above for h1 pointing out where and_assoc.mp is invoked?

Appreciate any light you or someone can shed on this.
Many Thanks,
Daniel

[Daniel Weber]

If I understand correctly, the thing you have trouble with is

example (P Q R : Prop) : (P ∧ Q ∧ R → False) → (P ∧ Q) ∧ R → False :=
  imp_trans and_assoc.mp

Do you know about currying? Try explicitly writing what A, B, C are in imp_trans (you can do that using imp_trans (A := _) (B := _) (C := _) and_assoc.mp)

[Richard Copley]

The type of and_assoc.mp is (a ∧ b) ∧ c → a ∧ b ∧ c.
The type of imp_trans is (X → Y) → ((Y → Z) → (X → Z)).
In order for imp_trans and_assoc.mp to make sense, the type of and_assoc.mp must match the first parameter of imp_trans.
That is, X → Y matches (a ∧ b) ∧ c → a ∧ b ∧ c.
Hence X is (a ∧ b) ∧ c and Y is a ∧ b ∧ c.
Therefore the type of h2 is (Y → Z) → (X → Z), or (a ∧ b ∧ c → Z) → ((a ∧ b) ∧ c → Z).

The type of h1 is (P ∨ Q) ∨ R → ((P ∧ Q ∧ R) → False) as you saw.

In order for imp_trans h1 h2 to be valid,

• the type of h1 : (P ∨ Q) ∨ R → ((P ∧ Q ∧ R) → False) must match A → B,
• the type of h2 : (a ∧ b ∧ c → Z) → ((a ∧ b) ∧ c → Z) must match B → C.

So (*),

• A matches (P ∨ Q) ∨ R
• B matches (P ∧ Q ∧ R) → False and also matches a ∧ b ∧ c → Z.
• C matches (a ∧ b) ∧ c → Z.

(We now see that imp_trans h1 h2 is of type A → C or, substituting, (P ∨ Q) ∨ R → ((a ∧ b) ∧ c → Z)).

Doing some further unification on (*), we deduce that a, b, c, Z respectively match P, Q, R, False.

Therefore imp_trans h1 h2 is of type (P ∨ Q) ∨ R → ((P ∧ Q) ∧ R → False), and that is what we wanted.

Is that any help?

[Daniel Bush]

Hi Richard,

Sorry for the delay and radio silence; had a horror end to last week, none of which relates to math or logic.

Richard Copley said:

....

Doing some further unification on (*), we deduce that a, b, c, Z respectively match P, Q, R, False.

Therefore imp_trans h1 h2 is of type (P ∨ Q) ∨ R → ((P ∧ Q) ∧ R → False), and that is what we wanted.

Is that any help?

The working you did helped.

I was not thinking through the currying properly. My brain was not trying to call imp_trans with and_assoc.mp . I was trying to think in terms of an additional function f where imp_trans and_assoc.mp f so I was wanting h2 to do X -> Z. Maybe the fact some types are unresolved or placeholders that need to match constraints was a bit too much for me to take in on top of clearly prosecuting that currying logic.

Thanks for getting me unstuck!
Daniel.

[Daniel Bush]

Daniel Weber said:

If I understand correctly, the thing you have trouble with is

example (P Q R : Prop) : (P ∧ Q ∧ R → False) → (P ∧ Q) ∧ R → False :=
  imp_trans and_assoc.mp

Do you know about currying? Try explicitly writing what A, B, C are in imp_trans (you can do that using imp_trans (A := _) (B := _) (C := _) and_assoc.mp)

Thanks for that tip and sorry for delay in reply. I was definitely not thinking through the currying logic properly, but I think I've got it straight now.

Cheers,
Daniel.