Add DHOL peano numbers theory to avoid including HOL one

Since the HOL Peano numbers theory includes simple function types with cause notation clashes with dependent function types.

source/casestudies/2023-cade/InductiveFixedLengthLists/lists.mmt

@@ -6,27 +6,27 @@ import base latin:/ ❚
 
 
 // A simple example theory that formalizes inductive lists of given length.❚ 
-theory Lists : latin:/?DHOL =
-		include ☞tptp?Peano ❙ 			
- 		// temporary workaround to fix some oneOf errors due to both the dependent-typed
- 			 and simple typed versions being included ❙
- 		deplam: {A,B} ({x: tm A} tm B x) ⟶ tm Πͭ B❘ = deplambda ❘# lam 3 prec 40❙
- 		depappl: {A,B} tm Πͭ B ⟶ {x: tm A} tm B x ❘ = depapply ❘# 3 appl 4 prec 50❙
+theory Lists : latin:/?DIHOL =
+		include ?Peano ❙
 
-    obj : tp ❙
-    list : {n: tm N} tp ❙
-    nil : tm (list zero) ❙
-    cons : tm Πͭ [n : tm N] Πͭ [x : tm obj] Πͭ [l : tm (list n)] (list (suc n)) ❙
+		obj : tp ❙
+		list : {n: tm N} tp ❙
+		nil : tm (list zero) ❙
+		cons : tm Πͭ [n : tm N] Πͭ [x : tm obj] Πͭ [l : tm (list n)] (list (suc n)) ❙
     
  		induction_N: {n: tp, z: tm n, s: tm Πͭ [m: tm n] n} {m: tm N} tm n ❙
  		addition = induction_N 
  			(Πͭ[m: tm N] N)
- 			(lam [x: tm N] x)
- 			(lam [u: tm Πͭ [m: tm N] N] lam [x: tm N] suc (u appl x)) ❙
- 		addn : tm N ⟶ tm N ⟶ tm N ❘ = [m, n] (addition m) appl n ❘# 1 plus 2 ❙
-		predec : {n: tm N} tm N ❘ = induction_N N zero (lam [u] u) ❙
+ 			(λ [x: tm N] x)
+ 			(λ [u: tm Πͭ [m: tm N] N] λ [x: tm N] suc (u @ x)) ❙
+ 		addn : tm N ⟶ tm N ⟶ tm N ❘ = [m, n] (addition m) @ n ❘# 1 plus 2 ❙
+		predec : {n: tm N} tm N ❘ = induction_N N zero (λ [u] u) ❙
 		convert: tm Πͭ [n : tm N] Πͭ [k : tm (list n)] list (zero plus n) ❙
  		
+		// to sidestep the below issues, however we cannot easily express the property
+		that piAppl is just β-reduction ❙
+		// piAppl: {t: tp, fun: {arg: tm t} tp, arg: tm t} tp ❘# 2 piAppl 3 ❙
+		
 		induction_list: {n: tm N, 
  			lst: {mp: tm N} tp, 
  			nl: tm (lst zero), 
@@ -36,23 +36,26 @@ theory Lists : latin:/?DHOL =
  		// For debugging the below errors. The issue is that MMT's type checker/solver 
  			 doesn't definition expand and then simplify types of the form 
  			 tm (lst mp)  to  Πͭ [lp : tm (list n)] list (mp plus n) ❙
+ 		// it should be possible to sidestep the problem using the structural feature 
+ 		for inductive types (see the (directly analogous) definition 
+ 		at MMT/examples/source/induction/basics.mmt),
+ 		but currently that feature doesn't support (inductively-defined) tps ❙
 		n: tm N ❙
 		// k: tm (list n) ❙
-		lst: Πͭ [mp : tm N] Πͭ [lp : tm (list n)] list (mp plus n) ❙
+		lst: {mp : tm N} Πͭ [lp : tm (list n)] list (mp plus n) ❙
 		nl : tm (lst zero) ❘ 
-		= lam [lp: tm (list n)] (convert appl n) appl lp ❙
+		= λ [lp: tm (list n)] (convert @ n) @ lp ❙
 		// cns // : tm Πͭ [m : tm N] Πͭ [x : tm obj] Πͭ [k : tm (lst m)] (lst (suc m)) ❘ = 
-		//	lam [mp: tm N] lam [x: tm obj] lam [concatK : tm Πͭ [lp: tm (list n)] list (mp plus n)] lam [lp: tm (list n)] 
-						(((cons appl (mp plus n)) appl x) appl (concatK appl lp)) ❙		
+		//	λ [mp: tm N] λ [x: tm obj] λ [concatK : tm Πͭ [lp: tm (list n)] list (mp plus n)] λ [lp: tm (list n)] 
+						(((cons @ (mp plus n)) @ x) @ (concatK @ lp)) ❙		
     
  		concat: tm Πͭ [m : tm N] Πͭ [k : tm (list m)] Πͭ [n : tm N] Πͭ [l : tm (list n)] list (m plus n) 
- 			❘ = lam [m] lam [k] lam [n] lam [l] 
+ 			❘ = λ [m] λ [k] λ [n] λ [l] 
 				(((induction_list m 
 					({mp : tm N} Πͭ [lp : tm (list n)] list (mp plus n))
-					(lam [lp: tm (list n)] (convert appl n) appl lp)
-					(lam [mp: tm N] lam [x: tm obj] lam [concatK : tm Πͭ [lp: tm (list n)] list (mp plus n)] lam [lp: tm (list n)] 
-						(((cons appl (mp plus n)) appl x) appl (concatK appl lp))
-					)) k) appl n) appl l
+					(λ [lp: tm (list n)] (convert @ n) @ lp)
+					(λ [mp: tm N] λ [x: tm obj] λ [concatK : tm Πͭ [lp: tm (list n)] list (mp plus n)] λ [lp: tm (list n)] 
+						(((cons @ (mp plus n)) @ x) @ (concatK @ lp))
+					)) k) @ n) @ l
  			❘ # 3 :: 4 ❙
-		
 ❚

source/casestudies/2023-cade/PeanoNumbers/peano.mmt

+namespace latin:/casestudies/_2023-cade❚
+
+theory Peano : latin:/?DHOLND =
+    N : tp❙
+    successor : tm (N → N)❙
+
+    // simple notation for successor application ❙
+    suc = [n: tm N] (successor @ n) ❙
+
+    zero : tm N❙
+
+    //No Confusion Axiom❙
+    axiom3 : ⊦ ∀ͭ[n: tm N] ¬(successor @ n =ͭ zero)❙
+
+    //Injectivity Axiom❙
+    axiom4 : ⊦ ∀ͭ[n: tm N] ∀ͭ[m: tm N] ((successor @ n =ͭ successor @ m) ⇒ (n =ͭ m))❙
+
+    //Induction Axiom❙
+    axiom5 : ⊦ ∀ͭ[X: tm N → bool] X @ zero ∧ (∀ͭ[n : tm N] X @ n ⇒ X @ (successor @ n)) ⇒ ∀ͭ[x: tm N] X @ x❙
+
+    // Conjecture❙
+    conj : ⊦ ∀ͭ[x: tm N] (x =ͭ zero) ∨ (∃ͭ[y: tm N] successor @ y =ͭ x) ❘ = PROVE❙
+
+    // simpler conjecture❙
+    conj2 : ⊦ ∀ͭ[x: tm N] ([z: tm N] z =ͭ x) zero ∨ (∃ͭ[y: tm N] ([z: tm N] z =ͭ x) (successor @ y)) ❘ = PROVE❙
+
+    // even simpler conjecture❙
+    p = [x: tm N] [z: tm N] z =ͭ x ❙
+    conj3 : ⊦ ∀ͭ[x: tm N] (p x) zero ∨ (∃ͭ[y: tm N] (p x) (successor @ y)) ❘ = PROVE❙
+
+    //decl2 = successor @ (successor @ zero)❙
+
+    //conj2 : ⊦ ¬(decl2 =ͭ zero) ❘ = PROVE❙
+❚

source/casestudies/2023-cade/test-mmt-based-prover.msl

@@ -34,6 +34,12 @@ extension latin2.tptp.DHOLExporter
 extension latin2.tptp.DPHOLExporter
 
 
+mathpath archive /home/user/Erlangen/MMT/content/MathHub/MMT/urtheories
+mathpath archive /home/user/Erlangen/MMT/content/MathHub/MMT/LATIN2
+mathpath archive /home/user/Erlangen/MMT/content/MathHub/MMT/examples
+mathpath archive /home/user/Erlangen/MMT/content/MathHub/MMT/LFX
+
+
 define dependencies
 	build MMT/urtheories mmt-omdoc lf.mmt
 	//build MMT/urtheories mmt-omdoc sequences.mmt
@@ -49,12 +55,16 @@ define dependencies
 	build MMT/LATIN2 mmt-omdoc logic/fol_like/sfol.mmt
 	build MMT/LATIN2 mmt-omdoc logic/hol_like/hol.mmt
 	build MMT/LATIN2 mmt-omdoc logic/hol_like/dhol.mmt
-	//build MMT/LATIN2 mmt-omdoc logic/fol.mmt
-	//build MMT/LATIN2 mmt-omdoc logic/pl.mmt
+	
+	build MMT/LFX mmt-omdoc TypedHierarchy.mmt
+	build MMT/examples mmt-omdoc induction/lfxi.mmt
+	//	build MMT/LATIN2 mmt-omdoc logic/fol.mmt
+	// build MMT/LATIN2 mmt-omdoc logic/pl.mmt
 	//build MMT/LATIN2 mmt-omdoc logic/stfol.mmt
 	//build MMT/LATIN2 mmt-omdoc foundations/mizar.mmt
 	//build MMT/LATIN2 mmt-omdoc foundations/mizar-patterns.mmt
 	build MMT/LATIN2 lf-scala fundamentals/concepts.omdoc
+	build MMT/LATIN2 mmt-omdoc casestudies/2023-cade/Peano
 end
 
 // do dependencies
@@ -64,3 +74,6 @@ end
 // test DPHOL exporter examples for CADE 2023 paper
 build MMT/LATIN2 mmt-omdoc casestudies/2023-cade/
 build MMT/LATIN2 tptp casestudies/2023-cade/
+
+//build MMT/LATIN2 mmt-omdoc casestudies/2023-cade/InductiveFixedLengthLists
+//build MMT/LATIN2 tptp casestudies/2023-cade/InductiveFixedLengthLists