Suitability comparing concrete languages and theories

[ppls-nd-prs]

Dear developers,

For some weeks I have been working with your Foundation library and am amazed by the universality of it and the extensive array of concepts it covers. I am currently working on a project where we have to compare two concrete languages ($\mathcal{L}_1$ and $\mathcal{L}_{2}$) and theories defined in those languages ($T_{\mathcal{L} 1}$, $T_{\mathcal{L}2}$). Due to your project's universality and the abstraction that goes along with it, I find it hard to gauge whether it would the right code to use for this rather more specific project.

One specific problem we run into is when we want to show that $T_{\mathcal{L} 1} \subseteq T_{\mathcal{L}2}$ (which we know is true). In order to achieve this we have to coerce the type $T_{\mathcal{L} 1}$ to type $T_{\mathcal{L}2}$, but we run into the problem that theories are sets of elements of type SyntacticFormula, with hence a fixed variable $n$, i.e. $n=0$, resulting in the error index in target's type is not a variable (consider using the cases tactic instead) 0, as the all and ex cases of the Semiformula type requires formulas with $n=n+1$.

A solution to this might be to formulate one language that can express everything in $\mathcal{L}_2$ and define $\mathcal{L}_1$ to be a subset of this directly. However, then we run into the problem that at some point we have to prove that the subset $\mathcal{L}_1$ is decidable, which again requires induction over SyntacticFormulas, which is again not possible due to the same problem as mentioned in the previous paragraph.

Do you, as developers, have any suggestion on how to best approach these problems?

I am looking forward to your answer.
Cheers.

[iehality]

Hi ppls-nd-prs.

Please let me know if I have misunderstood your problem.
First, I have been dealing only with relations between theories of the same language, so I think the gadget for comparisons between different languages is inadequate, but a suitable extension of the current one will do.

Let L₁ and L₂ be the Languages corresponding to the languages $\mathcal{L}_1$ and $\mathcal{L}2$ , and let T₁ and T₂ be the Theory L₁ and Theory L₂ corresponding to $T{\mathcal{L}1}$ and $T{\mathcal{L}_2}$ .
If the language L₁ is a subset of L₂ as a set of symbols, then we should construct a map Φ: L₁ →ᵥ L₂ Language.Hom (If this is not the case, we might need to use interpretation instead of the mapping, though interpretation is currently disabled). Then, we can show T₁.lMap Φ ⊆ T₂. However, in terms of theory comparison, the more generalized notion T₁.lMap Φ ⪯ T₂ might be easier to work with (Using Entailment.WeakerThan.ofSubset, we can derive the latter from the former).

And it seems that induction on Semiformulas is causing issues, but if you explicitly specify n as an argument, you should be able to define it (e.g. see the definition of lMapAux ). Also you can use termination_by φ => φ.complexity. e.g.:

Foundation/Foundation/FirstOrder/Basic/Calculus.lean

Lines 151 to 182 in 94d1821

	def em {Δ : Sequent L} : {φ : SyntacticFormula L} → (hpos : φ ∈ Δ) → (hneg : ∼φ ∈ Δ) → T ⟹ Δ
	| ⊤, hpos, hneg => verum' hpos
	| ⊥, hpos, hneg => verum' hneg
	| .rel R v, hpos, hneg => axL' R v hpos hneg
	| .nrel R v, hpos, hneg => axL' R v hneg hpos
	| φ ⋏ ψ, hpos, hneg =>
	have ihp : T ⟹ φ :: ∼φ :: ∼ψ :: Δ := em (φ := φ) (by simp) (by simp)
	have ihq : T ⟹ ψ :: ∼φ :: ∼ψ :: Δ := em (φ := ψ) (by simp) (by simp)
	have : T ⟹ ∼φ :: ∼ψ :: Δ := (ihp.and ihq).wk (by simp[hpos])
	this.or.wk (by simpa using hneg)
	| φ ⋎ ψ, hpos, hneg =>
	have ihp : T ⟹ ∼φ :: φ :: ψ :: Δ := em (φ := φ) (by simp) (by simp)
	have ihq : T ⟹ ∼ψ :: φ :: ψ :: Δ := em (φ := ψ) (by simp) (by simp)
	have : T ⟹ φ :: ψ :: Δ := (ihp.and ihq).wk (by simp [by simpa using hneg])
	this.or.wk (by simp[hpos])
	| ∀' φ, hpos, hneg =>
	have : T ⟹ ∼Rewriting.free φ :: Rewriting.free φ :: Δ⁺ := em (φ := Rewriting.free φ) (by simp) (by simp)
	have : T ⟹ (∼Rewriting.shift φ)/[&0] :: Rewriting.free φ :: Δ⁺ :=
	Derivation.cast this (by simp[←TransitiveRewriting.comp_app])
	have : T ⟹ Rewriting.free φ :: Δ⁺ := (ex &0 this).wk
	(List.cons_subset_of_subset_of_mem
	(List.mem_cons_of_mem (free φ) <| by simpa using mem_shifts_iff.mpr hneg) (by rfl))
	this.all.wk (by simp[hpos])
	| ∃' φ, hpos, hneg =>
	have : T ⟹ Rewriting.free φ :: ∼Rewriting.free φ :: Δ⁺ := em (φ := Rewriting.free φ) (by simp) (by simp)
	have : T ⟹ (Rewriting.shift φ)/[&0] :: ∼Rewriting.free φ :: Δ⁺ :=
	Derivation.cast this (by simp[←TransitiveRewriting.comp_app])
	have : T ⟹ Rewriting.free (∼φ) :: Δ⁺ := (ex &0 this).wk
	(List.cons_subset_of_subset_of_mem
	(List.mem_cons_of_mem (free (∼φ)) <| by simpa using mem_shifts_iff.mpr hpos) (by simp))
	this.all.wk (by simpa using hneg)
	termination_by φ => φ.complexity

Also, Semiformula.rec' can be useful.

Furthermore, if you want to use DecidableEq (Semiformula L ξ n), you just need to prove [∀ k, DecidableEq (L.Func k)], [∀ k, DecidableEq (L.Rel k)], and [DecidableEq ξ], see: LO.FirstOrder.Semiformula.instDecidableEq .

[ppls-nd-prs]

Hi iehality,

Yes, you have understood my question! Thank you for your quick reply and taking the time to answer. This helps me a lot! :)