Why does the termination_by drop my induction condition?

Stream: lean4

[Dongheng Chen]

I am a master's student working on formalizing the intuitionistic first order logic. In a proof of monotonic, I use induction on the formula g.

lemma Formula.mono_proof {σ : Signature}(M: model σ)(u v:M.world)(hr: M.R u v)(g: Formula σ)(hw: u ∈ M.W)(val:Term σ → M.A)(h1: g.force_form M u hw val ): g.force_form M v (M.R_closed u v hr hw) val:= by
  let depth:=g.size
  induction g with
  | atomic_formula r ts => unfold force_form at h1
                           unfold force_form
                           apply M.mono u v hw (M.R_closed u v hr hw) r (fun q => val (ts q)) hr h1
  | bottom => unfold force_form
              unfold force_form at h1
              assumption
  | conjunction f1 f2 => rename_i h3 h4
                         unfold force_form
                         apply And.intro
                         unfold force_form at h1
                         apply h3 h1.left
                         apply h4 h1.right
  | disjunction f1 f2 => rename_i h3 h4
                         unfold force_form
                         unfold force_form at h1
                         apply Or.elim h1
                         intro h5
                         apply Or.inl
                         apply h3 h5
                         intro h6
                         apply Or.inr
                         apply h4 h6
  | negation f => rename_i h0
                  unfold force_form
                  unfold force_form at h1
                  intro w2 hw2
                  apply h1
                  have h3: w2 ∈ M.W :=by apply M.R_closed v w2 hw2 (M.R_closed u v hr hw)
                  have h4: v ∈ M.W :=by apply M.R_closed u v hr hw
                  apply M.trans u hw v h4 w2 h3 hr hw2
  | implication f1 f2 f3 f4 => unfold force_form
                               unfold force_form at h1
                               intro w2 hw2
                               have h6: _ :=by apply strong_connected M u v w2 hw hr hw2
                               apply h1 w2 h6
  | existential_quantification f1 hv =>
                                have h0: f1.size<depth := by simp
                                unfold force_form
                                unfold force_form at h1
                                match h1 with
                                | ⟨t,ht⟩ =>  exact ⟨t,(Formula.mono_proof M u v hr f1 hw (modify_value_function M val t) ht)⟩

  | universal_quantification f2 hv =>
                                have h2: f2.size<depth := by simp
                                unfold force_form
                                unfold force_form at h1
                                intro t
                                sorry
  termination_by Formula.mono_proof M u v hr f hw val hz =>f.size
  decreasing_by

And I use

termination_by f.size

it requires me to provide the proof of

g.size > f1.size

The key problem occors here. When I try to prove it in

  decreasing_by

The infoview doesn't provide any information about the relation of g and f1. In fact, here we have g=(∃ᵢf1).
Now, I need to show g=(∃ᵢf1). But I can't do that.
My question is, Why termination_by eats my induction relation of f1 and g? Should I change a way of induction?

The whole file can be found here.
IFOL.lean

Thanks for any suggestion!

[Arthur Adjedj]

This works.

lemma Formula.mono_proof {σ : Signature}(M: model σ)(u v:M.world)(hr: M.R u v)(g: Formula σ)(hw: u ∈ M.W)(val:Term σ → M.A)(h1: g.force_form M u hw val ): g.force_form M v (M.R_closed u v hr hw) val:= by
  induction g generalizing val with
  | atomic_formula r ts => unfold force_form at h1
                           unfold force_form
                           apply M.mono u v hw (M.R_closed u v hr hw) r (fun q => val (ts q)) hr h1
  | bottom => unfold force_form
              unfold force_form at h1
              assumption
  | conjunction f1 f2 h3 h4 =>
                         unfold force_form
                         apply And.intro
                         unfold force_form at h1
                         apply h3 _ h1.left
                         apply h4 _ h1.right
  | disjunction f1 f2 h3 h4 =>
                         unfold force_form
                         unfold force_form at h1
                         apply Or.elim h1
                         intro h5
                         apply Or.inl
                         apply h3 _ h5
                         intro h6
                         apply Or.inr
                         apply h4 _ h6
  | negation f h0 =>
                  unfold force_form
                  unfold force_form at h1
                  intro w2 hw2
                  apply h1
                  have h3: w2 ∈ M.W :=by apply M.R_closed v w2 hw2 (M.R_closed u v hr hw)
                  have h4: v ∈ M.W :=by apply M.R_closed u v hr hw
                  apply M.trans u hw v h4 w2 h3 hr hw2
  | implication f1 f2 f3 f4 => unfold force_form
                               unfold force_form at h1
                               intro w2 hw2
                               have h6: _ :=by apply strong_connected M u v w2 hw hr hw2
                               apply h1 w2 h6
  | existential_quantification f hv =>
                                unfold force_form
                                unfold force_form at h1
                                match h1 with
                                | ⟨t,ht⟩ =>  exact ⟨t,hv (modify_value_function M val t) ht⟩
  | universal_quantification f hv =>
                                unfold force_form
                                unfold force_form at h1
                                intro t
                                exact hv (modify_value_function M val t) (h1 t)

I don't think you should mix using inductionand explicit recursion in your code, either do one or the other. I'm guessing that's what messed up the termination-checker here.

[Arthur Adjedj]

Also, you may prefer using term-mode for such proofs:

lemma Formula.mono_proof {σ : Signature}(M: model σ)(u v:M.world)(hr: M.R u v)(g: Formula σ)(hw: u ∈ M.W)(val:Term σ → M.A)(h1: g.force_form M u hw val ): g.force_form M v (M.R_closed u v hr hw) val :=
  match g with
  | atomic_formula r ts =>  M.mono u v hw (M.R_closed u v hr hw) r (fun q => val (ts q)) hr h1
  | bottom => ‹_›
  | conjunction f1 f2 => ⟨f1.mono_proof _ _ _ hr _ _ h1.left,f2.mono_proof _ _ _ hr _ _  h1.right⟩
  | disjunction f1 f2 => h1.elim (fun h5 => .inl <| f1.mono_proof _ _ _ hr _ _ h5) (fun h6 => .inr <| f2.mono_proof _ _ _ hr _ _ h6)
  | negation _ => fun w2 hw2 =>
    have h3: w2 ∈ M.W := M.R_closed v w2 hw2 (M.R_closed u v hr hw)
    have h4: v  ∈ M.W :=  M.R_closed u v hr hw
    h1 _ <| M.trans u hw v h4 w2 h3 hr hw2
  | implication _ _  => fun w2 hw2 =>
    have h6: _ :=  strong_connected M u v w2 hw hr hw2
    h1 w2 h6
  | existential_quantification f =>
    let ⟨t,ht⟩ := h1
    ⟨t,(Formula.mono_proof M u v hr f hw (modify_value_function M val t) ht)⟩
  | universal_quantification f => fun t =>
    Formula.mono_proof M u v hr f hw (modify_value_function M val t) (h1 t)