Help with complitacted induction proof

Stream: mathlib4

[Thomas Vigouroux]

Hey there ! Lately I have been asking a lot of questions related to some proofs I have been attempting to formalize in Lean4 about G4ip (a contraction-free sequent calculus for intuitionistic propositional logic).

Currently I am stuck because of a dependent elimination error, I am am somewhat puzzled by the problem.

Here is the code:

import Mathlib.Tactic
import Mathlib.Data.Finset.Basic

abbrev Variable := ℕ

inductive Formula
| bot
| var : Variable → Formula
| and : Formula → Formula → Formula
| or : Formula → Formula → Formula
| imp : Formula → Formula → Formula
deriving DecidableEq

instance : HAnd Formula Formula Formula where
  hAnd := Formula.and

instance : HOr Formula Formula Formula where
  hOr := Formula.or

abbrev Formula.not (G: Formula) := Formula.imp G .bot
abbrev Formula.top := not bot
abbrev Formula.equiv (A B: Formula) := (imp A B) &&& (imp B A)

notation:max (priority := high) "#" v:max => Formula.var v
infixr:27 (priority := high) " ⟹ " => Formula.imp

instance: Neg Formula where
  neg := Formula.not

instance: Bot Formula where
  bot := Formula.bot

instance: Top Formula where
  top := Formula.top

-- Model theory

variable {H : Type _} [HeytingAlgebra H]
@[simp]
def eval (v : Variable → H) : Formula → H
  | .bot    => ⊥
  | # P    => v P
  | A ||| B => eval v A ⊔ eval v B
  | A &&& B => eval v A ⊓ eval v B
  | A ⟹ B => eval v A ⇨ eval v B


/- We say that `A` is a consequence of `Γ` if for all valuations in any Heyting algebra, if
  `eval v B` is above a certain element for all `B ∈ Γ` then `eval v A` is above this element.
  Note that for finite sets `Γ` this corresponds exactly to
  `Infimum { eval v B | B ∈ Γ } ≤ eval v A`.
  This "yoneda'd" version of the definition of validity is very convenient to work with. -/
def Models (Γ : Finset Formula) (A : Formula) : Prop :=
  ∀ {H : Type} [HeytingAlgebra H] {v : Variable → H} {c}, (∀ B ∈ Γ, c ≤ eval v B) → c ≤ eval v A

local infix:27 (priority := high) " ⊨ " => Models
def Valid (A : Formula) : Prop := ∅ ⊨ A

set_option hygiene false
infix:27 (priority:=high) " ⊢ " => Sequent

inductive Sequent : Finset Formula → Formula → Prop
| Ax : A ∈ Γ  → Γ ⊢ A
| ExFalso : ⊥ ∈ Γ → Γ ⊢ G
| AndI : Γ ⊢ A → Γ ⊢ B → Γ ⊢ A &&& B
| AndE : insert A (insert B Γ) ⊢ C → insert (A &&& B) Γ ⊢ C
| OrI1 : Γ ⊢ A → Γ ⊢ (A ||| B)
| OrI2 : Γ ⊢ B → Γ ⊢ (A ||| B)
| OrE : insert A Γ ⊢ C → insert B Γ ⊢ C → insert (A ||| B) Γ ⊢ C
| ImpI : insert A Γ ⊢ B → Γ ⊢ (A ⟹ B)
-- Now the ImpE rules, that are exploded by cases
-- Γ, a, B ⊢ C → Γ, a, a ⇒ B ⊢ C
| ImpEAtom : insert A (insert B Γ) ⊢ C → insert A (insert (A ⟹ B) Γ) ⊢ C
| ImpEBot : Γ ⊢ C → insert (⊥ ⟹ B) Γ ⊢ C
| ImpEAnd : insert (A₁ ⟹ A₂ ⟹ B) Γ ⊢ C → insert ((A₁ &&& A₂) ⟹ B) Γ ⊢ C
| ImpEOr : insert (A₁ ⟹ B) (insert (A₂ ⟹ B) Γ) ⊢ C → insert ((A₁ ||| A₂) ⟹ B) Γ ⊢ C
| ImpEImp : insert A₁ (insert (A₂ ⟹ B) Γ) ⊢ A₂ → insert B Γ ⊢ C → insert ((A₁ ⟹ A₂) ⟹ B) Γ ⊢ C
-- ImpETop is not necessary see the lemma later

syntax "solve_mem": tactic
syntax "apply_ax": tactic
macro_rules
| `(tactic | solve_mem) => `(tactic |
  first
  | exact Finset.mem_singleton.mpr rfl
  | apply Finset.mem_insert_self
  | apply Finset.mem_insert_of_mem; solve_mem)
| `(tactic | apply_ax) => `(tactic | {apply Sequent.Ax; solve_mem})

lemma Sequent.ImpETop (h: insert B Γ ⊢ C) : insert (⊤ ⟹ B) Γ ⊢ C := by {
  apply Sequent.ImpEImp
  · apply_ax
  · exact h
}

lemma Sequent.AndE.invertible {Γ: Finset Formula} {A B C: Formula} (h: insert (A &&& B) Γ ⊢ C): insert A (insert B Γ) ⊢ C := by {
  cases h with
  | Ax h => {
    simp at h
    cases h with
    | inl h => {
      rw [h]
      apply AndI <;> apply_ax
    }
    | inr h => {
      apply Ax
      simp
      right
      right
      exact h
    }
  }
  | ExFalso h => {
    simp at h
    apply ExFalso
    simp
    right
    right
    exact h
  }
  | @AndI Γ A' B' hA hB => {
    apply AndI
    · exact Sequent.AndE.invertible hA
    · exact Sequent.AndE.invertible hB
  }
  | @OrI1 Γ A' B' hA => {
    apply OrI1
    exact Sequent.AndE.invertible hA
  }
  | @OrI2 Γ A' B' hB => {
    apply OrI2
    exact Sequent.AndE.invertible hB
  }
  -- dependent elimination failed
  | @AndE A' B' Γ' C hAB => sorry
  -- | AndE _ => sorry
  -- | OrE _ _ => sorry
  -- | ImpI _ => sorry
  -- | ImpEAtom _ => sorry
  -- | ImpEBot _ => sorry
  -- | ImpEAnd _ => sorry
  -- | ImpEOr _ => sorry
  -- | ImpEImp _ _ => sorry
}

[Thomas Vigouroux]

I realize that the example is a bit big, but it is mostly a modified version of GlimpseOfLean applied to the sequent calculus mentionned

[Thomas Vigouroux]

Another thing that surprised me is that changing the cases to a induction in the very last theorem causes an error stating the following:

index in target's type is not a variable (consider using the `cases` tactic instead)
  insert (A &&& B) Γ

[Mario Carneiro]

use generalize e : A &&& B = AB at h before induction

[Thomas Vigouroux]

Oh, I did not know about that generalize tactic, that's good for future use
Though doing that does not seem to fix the problem on my end

[Thomas Vigouroux]

Maybe I need to generalize e : insert (A &&& B) \Gamma = \Gamma' at h rather ?

[Mario Carneiro]

oh, yes you should

[Thomas Vigouroux]

So that seemed to fix the issue then, may I ask why it happened ?

[Mario Carneiro]

induction would otherwise lose information about the index at which you are applying the inductive type, you would be left with subgoals like Γ' ⊢ C -> insert A (insert B Γ) ⊢ C which are obviously not provable

[Mario Carneiro]

Proofs like this usually have to be careful / explicit about exactly how the index is generalized, because doing it wrong results in the wrong inductive hypothesis. The one I just showed means that you can only recurse on cases which don't change the context, meaning that OrI1 is okay but you may have difficulty with ImpEOr

[Mario Carneiro]

You may need to think a bit more carefully about what the induction hypothesis is here

[Thomas Vigouroux]

Hmm okay, I'll look into that carefully then

[Mario Carneiro]

Thinking about it some more, I think the theorem is provable with the generalize as I suggested, but you also need to use induction h generalizing Γ

[Thomas Vigouroux]

Hmm, probably, I'll try that then (I can't rn)

[Thomas Vigouroux]

So using the generalize as you suggested does not fix the problem about the index in the induction, which seems weird to me.

I am trying right now to do it using generalize e : insert (A &&& B) \Gamma = \Gamma' at h but while it helped in the beginning, it does not help much anymore

[Thomas Vigouroux]

Here is the (partial) proof at the moment (note that the case ImpI is done now):

lemma Sequent.AndE.invertible {Γ: Finset Formula} {A B C: Formula} (h: insert (A &&& B) Γ ⊢ C): insert A (insert B Γ) ⊢ C := by {
  generalize e : insert (A &&& B) Γ = Γ₀ at h
  induction h generalizing Γ with
  | @Ax A' Γ' h => {
    rw [← e] at h
    simp at h
    cases h with
    | inl h => {
      rw [h]
      apply AndI <;> apply_ax
    }
    | inr h => {
      apply Ax
      solve_mem
    }
  }
  | ExFalso h => {
    rw [← e] at h
    simp at h
    apply ExFalso
    solve_mem
  }
  | @AndI Γ A' B' hA hB IHA IHB => {
    apply AndI
    · exact IHA e
    · exact IHB e
  }
  | @ImpI A' Γ' B' hA IHA => {
    apply ImpI
    repeat rw [Finset.Insert.comm A']
    rw [← e] at hA
    rw [Finset.Insert.comm] at hA
    apply IHA
    rw [Finset.Insert.comm]
    congr
  }
  | OrI1 hA IHA => {
    apply OrI1
    exact IHA e
  }
  | OrI2 hB IHB => {
    apply OrI2
    exact IHB e
  }
  | @AndE A' B' Γ' C' hC' IHC' => {
    /-
    case AndE
    H : Type ?u.59957
    inst✝ : HeytingAlgebra H
    A B C : Formula
    Γ₀ : Finset Formula
    A' B' : Formula
    Γ' : Finset Formula
    C' : Formula
    hC' : Sequent (insert A' (insert B' Γ')) C'
    IHC' : ∀ {Γ : Finset Formula}, insert (A &&& B) Γ = insert A' (insert B' Γ') → Sequent (insert A (insert B Γ)) C'
    Γ : Finset Formula
    e : insert (A &&& B) Γ = insert (A' &&& B') Γ'
    ⊢ Sequent (insert A (insert B Γ)) C'
    -/
  }
  | @OrE A' Γ' C' B' hA' hB' IHA' IHB' => {
    sorry
  }
  | @ImpEAtom A' B' Γ' C hC IHC => sorry
  | ImpEBot _ => sorry
  | ImpEAnd _ => sorry
  | ImpEOr _ => sorry
  | ImpEImp _ _ => sorry
}

[Thomas Vigouroux]

I can't really find a way to use the insert (A &&& B) \Gamma = insert (A' &&& B') \Gamma' to my advantage though, and that seems to be the main culprit

[Thomas Vigouroux]

It seems that my induction principle is a little off, but I quite can't come up with another one.

My intuition would be to make it simpler by inducting on the "height" of a derivaion, but I can't come up with a good way of defining the height for some reason

[Thomas Vigouroux]

This gives me an error:

def Sequent.height: Γ ⊢ C → ℕ
/-
tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Sequent.casesOn' can only eliminate into Prop

Γ: Finset Formula
C: Formula
x✝¹: Sequent Γ C
motive: Sequent Γ C → Sort ?u.60142
h_1: (a : C ∈ Γ) → motive _
a✝¹: Finset Formula
a✝: Formula
x✝: Sequent a✝¹ a✝
⊢ Γ = a✝¹ → C = a✝ → HEq x✝¹ x✝ → motive x✝¹
 after processing
  _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
-/
| Ax _ => 0

[Thomas Vigouroux]

I think I will give up on trying to prove this, I really simply can't come up with a correct way to formulate my induction hypothesis to make it work

[Thomas Vigouroux]

So, reworking the definition of my inductive type, I now include the height of the derivation _in_ the inductive type, such that Sequent G A n represents derivations From G to A with size n

[Mario Carneiro]

@Thomas Vigouroux your last proof doesn't work for me, solve_mem fails in two cases

[Thomas Vigouroux]

Oh I think I changed the definition of the macro to include assumption as a first clause in the first block

[Mario Carneiro]

I've also exceeded my budget to think about this, but my recommendation would be to try to prove

lemma Sequent.mono {Γ Γ': Finset Formula} (h1 : Γ ⊆ Γ') (h: Γ ⊢ C) : Γ' ⊢ C := sorry

lemma Sequent.AndE.invertible {Γ: Finset Formula} {A B C: Formula}
    (h: Γ ⊢ C) : insert A (insert B (Γ \ {A &&& B})) ⊢ C := sorry

and do cases on whether A &&& B is equal to A' &&& B' in the AndE case

[Thomas Vigouroux]

Okay so here is the new proof I am attempting (complete file for completeness):

import Mathlib.Tactic
import Mathlib.Data.Finset.Basic

abbrev Variable := ℕ

inductive Formula
| bot
| var : Variable → Formula
| and : Formula → Formula → Formula
| or : Formula → Formula → Formula
| imp : Formula → Formula → Formula
deriving DecidableEq

instance : HAnd Formula Formula Formula where
  hAnd := Formula.and

instance : HOr Formula Formula Formula where
  hOr := Formula.or

abbrev Formula.not (G: Formula) := Formula.imp G .bot
abbrev Formula.top := not bot
abbrev Formula.equiv (A B: Formula) := (imp A B) &&& (imp B A)

notation:max (priority := high) "#" v:max => Formula.var v
infixr:27 (priority := high) " ⟹ " => Formula.imp

instance: Neg Formula where
  neg := Formula.not

instance: Bot Formula where
  bot := Formula.bot

instance: Top Formula where
  top := Formula.top

-- Model theory

variable {H : Type _} [HeytingAlgebra H]
@[simp]
def eval (v : Variable → H) : Formula → H
  | .bot    => ⊥
  | # P    => v P
  | A ||| B => eval v A ⊔ eval v B
  | A &&& B => eval v A ⊓ eval v B
  | A ⟹ B => eval v A ⇨ eval v B


/- We say that `A` is a consequence of `Γ` if for all valuations in any Heyting algebra, if
  `eval v B` is above a certain element for all `B ∈ Γ` then `eval v A` is above this element.
  Note that for finite sets `Γ` this corresponds exactly to
  `Infimum { eval v B | B ∈ Γ } ≤ eval v A`.
  This "yoneda'd" version of the definition of validity is very convenient to work with. -/
def Models (Γ : Finset Formula) (A : Formula) : Prop :=
  ∀ {H : Type} [HeytingAlgebra H] {v : Variable → H} {c}, (∀ B ∈ Γ, c ≤ eval v B) → c ≤ eval v A

local infix:27 (priority := high) " ⊨ " => Models
def Valid (A : Formula) : Prop := ∅ ⊨ A

instance hABool: HeytingAlgebra Bool where
  bot_le := by {
    intro a
    cases a <;> simp
  }
  himp_bot := by {
    intro a
    cases a <;> simp [himp]
  }

-- Provability

set_option hygiene false
infix:27 (priority:=high) " ⊢ " => Sequent

inductive Sequent : Finset Formula → Formula → Prop
| Ax : A ∈ Γ → Γ ⊢ A
| ExFalso : ⊥ ∈ Γ → Γ ⊢ G
| AndI : Γ ⊢ A → Γ ⊢ B → Γ ⊢ A &&& B
| AndE : insert A (insert B Γ) ⊢ C → insert (A &&& B) Γ ⊢ C
| OrI1 : Γ ⊢ A → Γ ⊢ (A ||| B)
| OrI2 : Γ ⊢ B → Γ ⊢ (A ||| B)
| OrE : insert A Γ ⊢ C → insert B Γ ⊢ C → insert (A ||| B) Γ ⊢ C
| ImpI : insert A Γ ⊢ B → Γ ⊢ (A ⟹ B)
-- Now the ImpE rules, that are exploded by cases
-- Γ, a, B ⊢ C → Γ, a, a ⇒ B ⊢ C
| ImpEAtom : insert A (insert B Γ) ⊢ C → insert A (insert (A ⟹ B) Γ) ⊢ C
| ImpEBot : Γ ⊢ C → insert (⊥ ⟹ B) Γ ⊢ C
| ImpEAnd : insert (A₁ ⟹ A₂ ⟹ B) Γ ⊢ C → insert ((A₁ &&& A₂) ⟹ B) Γ ⊢ C
| ImpEOr : insert (A₁ ⟹ B) (insert (A₂ ⟹ B) Γ) ⊢ C → insert ((A₁ ||| A₂) ⟹ B) Γ ⊢ C
| ImpEImp : insert A₁ (insert (A₂ ⟹ B) Γ) ⊢ A₂ → insert B Γ ⊢ C → insert ((A₁ ⟹ A₂) ⟹ B) Γ ⊢ C
-- ImpETop is not necessary see the lemma later

-- Because this is a recursive macro, this has to be done in two parts
lemma finset_extract [DecidableEq α] {A: α} {S: Finset α} (h: A ∈ S): ∃S', (insert A S' = S) ∧ A ∉ S' := by {
  exists S.erase A
  constructor
  · exact Finset.insert_erase h
  · exact Finset.not_mem_erase A S
}

syntax "solve_mem": tactic
macro_rules
| `(tactic | solve_mem) => `(tactic |
  first
  | trivial
  | exact Finset.mem_singleton.mpr rfl
  | apply Finset.mem_insert_self
  | apply Finset.mem_insert_of_mem; solve_mem)
macro "apply_ax": tactic => `(tactic | {apply Sequent.Ax; solve_mem})

lemma Sequent.ImpETop (h: insert B Γ ⊢ C) : insert (⊤ ⟹ B) Γ ⊢ C := by {
  apply Sequent.ImpEImp
  · apply_ax
  · exact h
}

lemma Sequent.mono (h: Γ ⊆ Δ) (hΓ: Γ ⊢ A): Δ ⊢ A := by {
  induction hΓ generalizing Δ with
  | Ax h' => exact Sequent.Ax (h h')
  | ExFalso h' => exact Sequent.ExFalso (h h')
  | AndI hA hB IHA IHB => {
    apply AndI
    · exact IHA h
    · exact IHB h
  }
  | ImpI h' IH => {
    apply ImpI
    apply IH
    exact Finset.insert_subset_insert _ h
  }
  | OrI1 h' IH => {
    apply OrI1
    exact IH h
  }
  | OrI2 h' IH => {
    apply OrI2
    exact IH h
  }
  | @AndE A B Γ C h' IH => {
    if hAB: A &&& B ∈ Γ then {
      obtain ⟨Γ', ⟨hΓ', hΓ'nm⟩⟩ := finset_extract hAB
      have hΓ : insert (A &&& B) Γ = Γ
      · exact Finset.insert_eq_self.mpr hAB
      rw [hΓ] at h
      rw [← hΓ'] at h

      obtain ⟨Δ', ⟨hΔ', hΔ'nm⟩⟩ := finset_extract (S:=Δ) (A:=A &&& B) (by {
        apply h
        simp
      })
      rw [← hΔ']
      apply AndE
    } else {
      obtain ⟨Δ', ⟨hΔ', hΔ'nm⟩⟩ := finset_extract (S:=Δ) (A:=A &&& B) (by {
        apply h
        simp
      })
      rw [← hΔ']
      apply AndE
      apply IH
      apply Finset.insert_subset_insert
      apply Finset.insert_subset_insert
      apply (Finset.insert_subset_insert_iff hAB).mp
      rw [← hΔ'] at h
      exact h
    }
  }
  | OrE _ _ _ _ => sorry
  | ImpEAtom _ _ => sorry
  | ImpEBot _ _ => sorry
  | ImpEAnd _ _ => sorry
  | ImpEOr _ _ => sorry
  | ImpEImp _ _ _ _ => sorry
}

[Thomas Vigouroux]

I am already stuck at the AndE case, when A &&& B \in \Gamma, in this case, my intuition is that I can just reduce to a case with a \Gamma' sucha that A &&& B \notin \Gamma', but the induction hypothesis is wrong in this case.

[Mario Carneiro]

I don't think you need to do cases on A &&& B \in Gamma to prove monotonicity

[Thomas Vigouroux]

I thought too, but I can't find the theorem I'd need to avoid the cases on that

[Thomas Vigouroux]

Okay so I think I found the correct way to state the theorem for the proof to work, the thing I am now proving is:

lemma Sequent.mono (hΓ: Γ ⊢ A): Γ ∪ Δ ⊢ A

Which is much esaier to prove because of the union

[Thomas Vigouroux]

Here's the complete proof:

lemma Sequent.weakening (hΓ: Γ ⊢ A): Γ ∪ Δ ⊢ A := by {
  induction hΓ with
  | Ax h' => {
    apply Ax
    exact Finset.mem_union_left Δ h'
  }
  | ExFalso h' => {
    apply ExFalso
    exact Finset.mem_union_left Δ h'
  }
  | AndI _ _ IHA IHB => {
    apply AndI
    · exact IHA
    · exact IHB
  }
  | ImpI _ IH => {
    apply ImpI
    rw [← Finset.insert_union]
    exact IH
  }
  | OrI1 _ IH => {
    apply OrI1
    exact IH
  }
  | OrI2 _ IH => {
    apply OrI2
    exact IH
  }
  | AndE _ IH => {
    rw [Finset.insert_union]
    apply AndE
    repeat rw [← Finset.insert_union]
    exact IH
  }
  | ImpEAtom _  IH => {
    repeat rw [Finset.insert_union]
    apply ImpEAtom
    repeat rw [← Finset.insert_union]
    exact IH
  }
  | OrE _ _ IHA IHB => {
    rw [Finset.insert_union]
    apply OrE <;> rw [← Finset.insert_union]
    · exact IHA
    · exact IHB
  }
  | ImpEBot _ IH => {
    rw [Finset.insert_union]
    apply ImpEBot
    exact IH
  }
  | ImpEAnd _ IH => {
    rw [Finset.insert_union]
    apply ImpEAnd
    rw [← Finset.insert_union]
    exact IH
  }
  | ImpEOr _ IH => {
    rw [Finset.insert_union]
    apply ImpEOr
    repeat rw [← Finset.insert_union]
    exact IH
  }
  | ImpEImp _ _ IHA IHC => {
    rw [Finset.insert_union]
    apply ImpEImp <;> repeat rw [← Finset.insert_union]
    · exact IHA
    · exact IHC
  }
}

theorem Sequent.mono (h: Γ ⊆ Δ) (hΓ: Γ ⊢ C): Δ ⊢ C := by {
  generalize hΔ': Δ \ Γ = Δ'
  have hΔ : Δ = Γ ∪ Δ'
  · rw [← hΔ']
    simp
    exact h
  rw [hΔ]
  exact weakening hΓ
}