Puzzle proving using rewrites

Stream: new members

[FrenchNoodles]

Hello

I have the following code, as a "template" to use to prove "m1"

axiom v1 : Prop -- l’affirmation du coffre n°1 est vraie
axiom v2 : Prop -- l’affirmation du coffre n°2 est vraie
axiom v3 : Prop -- l’affirmation du coffre n°3 est vraie

axiom m1 : Prop -- le manuscrit se trouve dans le coffre n°1
axiom m2 : Prop -- le manuscrit se trouve dans le coffre n°2
axiom m3 : Prop -- le manuscrit se trouve dans le coffre n°3

axiom existe_manuscrit : m1 ∨ m2 ∨ m3
axiom coffre1 : v1 ↔ v2 ∧ m3
axiom coffre2 : v2 ↔ (¬v1 ∨ ¬v2) ∧ (¬v1 ∨ ¬v3) ∧ (¬v2 ∨ ¬v3)
axiom coffre3 : v3 ↔ m2

/- En utilisant les tactiques apply et rewrite, vous pouvez utiliser
   les théorèmes suivants dans votre raisonnement -/
theorem not_not_elim (p : Prop) : ¬¬p ↔ p := by
  apply Iff.intro
  case mp =>
    intro hnot_not_p
    by_cases hp : p
    case pos => apply hp
    case neg =>
      exfalso
      apply hnot_not_p
      apply hp
  case mpr =>
    intro hp
    intro hnot_p
    apply hnot_p
    apply hp

theorem or_not_left_elim (p : Prop) (q : Prop) : p ∨ q → ¬p → q := by
  intro hp_or_q
  intro hnot_p
  apply (Or.elim hp_or_q)
  case left =>
    intro hp
    exfalso
    apply hnot_p
    apply hp
  case right =>
    intro hq
    apply hq

theorem or_not_right_elim (p : Prop) (q : Prop) : p ∨ q → ¬q → p := by
  intro hp_or_q
  intro hnot_p
  apply (Or.elim hp_or_q)
  case left =>
    intro hq
    apply hq
  case right =>
    intro hp
    exfalso
    apply hnot_p
    apply hp

theorem de_morgan_and (p : Prop) (q : Prop) : ¬(p ∧ q) ↔ (¬p ∨ ¬q) := by
  apply Iff.intro
  case mp =>
    intro hnot_p_and_q
    by_cases hp : p
    case pos =>
      by_cases hq : q
      case pos =>
        exfalso
        apply hnot_p_and_q
        apply And.intro
        . apply hp
        . apply hq
      case neg =>
        right
        apply hq
    case neg =>
      left
      apply hp
  case mpr =>
    intro hnot_p_or_not_q
    intro hp_and_q
    apply (Or.elim hnot_p_or_not_q)
    case left =>
      intro hnot_p
      apply hnot_p
      apply hp_and_q.left
    case right =>
      intro hnot_q
      apply hnot_q
      apply hp_and_q.right

theorem de_morgan_or (p : Prop) (q : Prop) : ¬(p ∨ q) ↔ (¬p ∧ ¬q) := by
  apply Iff.intro
  case mp =>
    intro hnot_p_or_q
    apply And.intro
    case left =>
      intro hp
      apply hnot_p_or_q
      left
      apply hp
    case right =>
      intro hq
      apply hnot_p_or_q
      right
      apply hq
  case mpr =>
    intro hnot_p_and_not_q
    intro hp_or_q
    apply (Or.elim hp_or_q)
    case left =>
      intro hp
      apply hnot_p_and_not_q.left
      apply hp
    case right =>
      intro hq
      apply hnot_p_and_not_q.right
      apply hq

I tried doing the m1 proof but im having errors related to rewrites im not sure how to fix

/- Prouvez l’un des trois théorèmes suivants, selon votre déduction -/
  theorem reponse_m1 : m1 := by
-- Use the existence axiom to split cases
  cases existe_manuscrit with
  | inl h1 =>
    -- Case: m1 is true
    exact h1
  | inr h =>
    cases h with
    | inl h2 =>
      -- Case: m2 is true
      have h_v3 : v3 := by
        rewrite [coffre3]
        exact h2
      have h_v2 : v2 := by
        rewrite [coffre2] at h_v3
        rewrite [not_not_elim] at h_v3
        exact h_v3
      rewrite [coffre1] at h_v2
      cases h_v2 with
      | intro h_v2' h_m3 =>
        exfalso
        exact h_m3 -- This contradicts the current case assumption
    | inr h3 =>
      -- Case: m3 is true
      have h_v1_v2 : v1 := by
        rewrite [coffre1] at h3
        cases h3 with
        | intro h_v1 h_m3' =>
          exact h_v1
      have h_v2_or_v3 := by
        rewrite [coffre2] at h_v1_v2
        exact h_v1_v2
      exfalso
      apply h_v2_or_v3
      rewrite [de_morgan_and]
      exact h3

Can anyone help me fix this proof?

[FrenchNoodles]

I was converting the correct code from coq to lean, if needed I could provide the working correct Coq code.

[Etienne Marion]

What's the paper proof?

[FrenchNoodles]

So the question is, there are 3 chests, each containing a message,

Chest 1: the message in chest 2 is true, and the manuscript is in chest 3
Chest 2: In the 3 chests there is at most 1 right affirmation
Chest 3: The manuscript is in chest 2

So in natural language (im guessing thats paper proof?) we could say the manuscript is in chest 1, if we assume v2 (message of chest 2) is true, then, v1 and v3 are incorrect, if v1 is incorrect and v2 is correct then according to v1, m1 is correct.
Which concludes as the message in chest 2 is true and the manuscript is in chest 1

[FrenchNoodles]

This is the complete proof in Coq

Require Import Classical ClassicalFacts.

Axiom v1 : Prop.
Axiom v2 : Prop.
Axiom v3 : Prop.

Axiom m1 : Prop.
Axiom m2 : Prop.
Axiom m3 : Prop.

Axiom existe_manuscrit : m1 \/ m2 \/ m3.
Axiom coffre1 : v1 <-> v2 /\ m3.
Axiom coffre2 : v2 <-> (~v1 \/ ~v2) /\ (~v1 \/ ~v3) /\ (~v2 \/ ~v3).
Axiom coffre3 : v3 <-> m2.

Axiom LEM : excluded_middle.

Theorem reponse_m1 : m1.
  Proof with auto.
    destruct existe_manuscrit as [H1|[H2|H3]]...
    - apply coffre3 in H2.
      destruct (LEM v2) as [HT|HF].
      * assert (H : v2)...
        apply coffre2 in HT; intuition.
      * assert (H : ~v2)...
        apply (not_iff_compat coffre2) in HF.
        apply not_and_or in HF.
        destruct HF as [Ha|HF].
        + apply not_or_and in Ha as (H' & H'').
          apply NNPP in H''; congruence.
        + apply not_and_or in HF.
          destruct HF as [Hb|Hc].
          { apply not_or_and in Hb as (H' & H'').
            apply NNPP in H'. apply coffre1 in H' as []; congruence. }
          { apply not_or_and in Hc as (H' & H'').
            apply NNPP in H'; congruence. }
    - destruct (LEM v2) as [HT|HF].
      * assert (H : v2 /\ m3)...
        apply coffre1 in H.
        assert (H' : v2)...
        apply coffre2 in HT; intuition.
      * assert (H : ~v2)...
        apply (not_iff_compat coffre2) in HF.
        apply not_and_or in HF.
        destruct HF as [Ha|HF].
        + apply not_or_and in Ha as (H' & H'').
          apply NNPP in H''; congruence.
        + apply not_and_or in HF.
          destruct HF as [Hb|Hc].
          { apply not_or_and in Hb as (H' & H'').
            apply NNPP in H'. apply coffre1 in H' as []; congruence. }
          { apply not_or_and in Hc as (H' & H'').
            apply NNPP in H'; congruence. }
Qed.

But I need it in lean,and the above is my attempt, but its giving me errors that Im not sure how to fix

[Etienne Marion]

My bad I did not see that you had sent your attempted proof. The errors you get come from the fact that you want to rewrite using A <-> B, but this will only work if A appears at the place you want to rewrite, and it's not the case at the places you want to rewrite.

[FrenchNoodles]

How can I fix that?

[FrenchNoodles]

I think the entire lean "translation" is incorrect after further investigating

[Etienne Marion]

Well I don't know how to read Coq but indeed the translation seems to be wrong

[FrenchNoodles]

yeah I thought it was only a few errors, but even if those are fixed more are to come,
Im not sure what to do

[Etienne Marion]

Is the tactic intuition in Coq used to prove a goal by only using intuitionistic logic? If so I think this proof will be hard to translate, at least I do not know such tactic. There is tauto but it uses classical logic so it will solve everything instantly but I'm guessing it is not what you are looking for. Otherwise you'd have to make the steps taken by intuition explicit which could lengthen the proof.

[FrenchNoodles]

Is there a simple way the proof could be made? It doesnt necessarily have to be a translation of the coq one, but Im using the coq one since its the closest lead I have to a complete solution in lean

[Etienne Marion]

There you go:

theorem reponse_m1 : m1 := by
  have := existe_manuscrit
  have := coffre1
  have := coffre2
  have := coffre3
  tauto

[FrenchNoodles]

Oh-
I didnt really mean the tauto way, since as you said this solves everything instantly

[FrenchNoodles]

Im guessing Im supposed to prove it the normal way

[FrenchNoodles]

Although this solution is giving me errors anyways

[Etienne Marion]

You may need to add

import Mathlib.Tactic

at the top of the file

[Edward van de Meent]

by the way, using variable is preferred over axiom, just in case they might be inconsistent

[Edward van de Meent]

the following should work just as well:

variable {v1 : Prop} -- l’affirmation du coffre n°1 est vraie
variable {v2 : Prop} -- l’affirmation du coffre n°2 est vraie
variable {v3 : Prop} -- l’affirmation du coffre n°3 est vraie

variable {m1 : Prop} -- le manuscrit se trouve dans le coffre n°1
variable {m2 : Prop} -- le manuscrit se trouve dans le coffre n°2
variable {m3 : Prop} -- le manuscrit se trouve dans le coffre n°3

variable (existe_manuscrit : m1 ∨ m2 ∨ m3)
  (coffre1 : v1 ↔ v2 ∧ m3)
  (coffre2 : v2 ↔ (¬v1 ∨ ¬v2) ∧ (¬v1 ∨ ¬v3) ∧ (¬v2 ∨ ¬v3))
  (coffre3 : v3 ↔ m2)

[FrenchNoodles]

The first few lines were supplied by the prof Im not really allowed to change them

[FrenchNoodles]

Although im not sure if tactics are allowed, like "import Mathlib.Tactic"
He did state that theorems from mathlib4 are allowed tho, does this count as one?

[FrenchNoodles]

But I think the response normally expected doesnt require any outside imports

[Etienne Marion]

You can't use mathlib4 if you do not import anything. Tactics are not really theorems, but coding without tactic would be impossible (you couldn't use apply and rewrite for instance).

[Etienne Marion]

Now if you are only allowed to use apply, cases and rw I think this might be quite long.

[FrenchNoodles]

I think that's the case, I think we are supposed to use the most basic elements

[Philippe Duchon]

I am not sure what the exercise is supposed to be. It is not pure intuitionistic logic; the direct part of de_Morgan_and cannot be proved in intuitionistic logic (also, the Coq axioms include the excluded middle). So, is the goal to just use applys and rewrites (plus the supplied theorems) to get to one of the goals? (In this, Coq and Lean/Mathlib might be subtly different, the seemingly equivalent tactics might behave differently in some cases)

[Philippe Duchon]

The natural language proof seems to start with a proof by cases on v2 (or, excluded middle on v2), but the Coq proof starts by a proof by cases on existe_manuscrit (thus, prove that each of m2 and m3 leads to either a contradiction, or the conclusion m1).

[Philippe Duchon]

Unless I am misunderstanding what happens in my experiments, writing axiom existe_manuscrit: m1 \/ m2 \/ m3 results in an axiom that asserts that for any three propositions, one of them is true; this is clearly not what you want.

You can declare your various "axioms" as simple variables, but then if you want to use them in your proofs of theorems, you should add an include v1 v2 v3 m1 m2 m3 existe_manuscrit coffre1 coffre2 coffre3 command before you start writing your theorems (I got this from Lean's contextual help: variables that are not explicitly included in the statement of a theorem cannot be used in its proof; this is clearly in contrast with how Coq works). After that Lean will complain that you have lots of unused variables in your theorems, but these are just warnings and can be ignored.

[Edward van de Meent]

Philippe Duchon said:

Unless I am misunderstanding what happens in my experiments, writing axiom existe_manuscrit: m1 \/ m2 \/ m3 results in an axiom that asserts that for any three propositions, one of them is true; this is clearly not what you want.

you might be missing the axiom declarations for m1,m2,m3. if you have those too, this won't be an issue.

[Edward van de Meent]

you can check you have these by including set_option autoImplicit false at the top of your file.

[Riccardo Brasca]

This conversation is probably relevant

[Philippe Duchon]

Edward van de Meent said:

Philippe Duchon said:

Unless I am misunderstanding what happens in my experiments, writing axiom existe_manuscrit: m1 \/ m2 \/ m3 results in an axiom that asserts that for any three propositions, one of them is true; this is clearly not what you want.

you might be missing the axiom declarations for m1,m2,m3. if you have those too, this won't be an issue.

I thought I had tried it both with m1, m2, m3 as axioms and as variables, but apparently I didn't.

The conversation linked by Riccardo makes things clearer to me.

In retrospect, I am not sure what I expected a declaration such as axiom v1: Prop to mean. Is it just asserting the existence of some Prop named v1? (of course now I understand is has the side effect of making another declaration axiom av: v1 be about a specific Prop rather than just a blanket assumption that everything is true; but does it have other uses?)

[Edward van de Meent]

Philippe Duchon said:

Is it just asserting the existence of some Prop named v1?

exactly right! :100:
Do note that it doesn't say anything about distinctness from True or False

[FrenchNoodles]

Hello
Sorry for being late !
Yeah its just declaring the existence of v1, since in this context v1 means "the statement in the first chest is correct"
If I understood correctly I believe Im supposed to prove v2, and also prove that no-v2 is false

[FrenchNoodles]

Sorry to be more presice I meant to prove "coffre2"
v2 ↔ (¬v1 ∨ ¬v2) ∧ (¬v1 ∨ ¬v3) ∧ (¬v2 ∨ ¬v3)
Since v2 and coffre2 are interchangeable, v2 can be proved by proving this, using "tiers-exclu", a direct translation of that to english is "third party excluded" not sure if thats a correct translation, but basically im supposed to prove v2 as correct, and its opposite as incorrect.

[FrenchNoodles]

I also verified again and tauto is not allowed, the proof has to be written manually, im currently trying to write it in natural language

[Philippe Duchon]

"Tiers exclus" is "excluded middle" in English; the third party has to sit in the middle between "true" and "false". Or so it looks.

I solved the puzzle (without automation) in both Coq and Lean, each time relying on the excluded middle v2 or not v2; I did not restrict myself to apply and rw, if that's the goal. One way to proceed, at least to help visualize things, is to prove other equivalence lemmas for v2, getting rid of v2 in the RHS. Oh, and when rewriting your v2 or not v2 hypothesis, keep a copy of it, it helps when you need to come back for a contradiction. (Is there a tactic in Lean dedicated to making a copy of a hypothesis? I relied on have h' := h)