type refinement nonsense

source/arithmetics/naturals.mmt

 namespace http://mathhub.info/MitM/smglom/arithmetics ❚
 
 import base http://mathhub.info/MitM/Foundation ❚
+import lfxcop http://gl.mathhub.info/MMT/LFX/Coproducts❚
 
 theory NaturalNumbers : base:?Logic =
 	include base:?NatLiterals ❙
@@ -75,6 +76,10 @@ theory NaturalArithmetics : base:?Logic =
 	/T usefull lemmata for simple arithmetics ❙
     lemma_lt_pred_lt : {x : ℕ , n : ℕ } ⊦ `?NaturalNumbers?succ  x < n ⟶ ⊦ x < n ❘# lt_pred_lt 3❙
     lemma_le_pred_le : {x : ℕ , n : ℕ } ⊦ (`?NaturalNumbers?succ : ℕ ⟶ ℕ) x ≤ n ⟶ ⊦ x ≤ n ❘# le_pred_le 3❙
+    lemma_zero_le : {n : ℕ} ⊦ 0 ≤ n ❘ # lemma_zero_le 1 ❙
+    lemma_zero_succ_lt : {n : ℕ} ⊦ 0 < `?NaturalNumbers?succ  n ❘# lemma_zero_succ_lt 1 ❙
+
+
     // added by sw ❙
     // this one is needed to create a possibly empty subset of the natural numbers (this way we can create empty finite sequences)❙
     /T finite subset of the natural numbers ❙
@@ -168,3 +173,14 @@ theory INatProps : base:?Logic =
     // lemma_le_Suc_le ❙
 ❚
 
+
+theory CompDec : base:?Logic =
+    include ?NaturalArithmetics ❙
+    include lfxcop:?LFCoprod❙
+
+
+    le_dec : {a : ℕ} {b : ℕ} ((⊦ a ≤ b) ⨁ (⊦ b < a)) ❙
+    le_dec_b : {n : ℕ} ⊦ le_dec 0 n ≐  ((lemma_zero_le n) ↪l (⊦ n < 0)) ❙
+    le_dec_b2 : {n : ℕ}  ⊦ le_dec (`?NaturalNumbers?succ n) 0 ≐  ((⊦ (`?NaturalNumbers?succ n) ≤ 0 ) r↩ (lemma_zero_succ_lt n)) ❙
+    le_dec_S : {n : ℕ} {m : ℕ} ⊦ le_dec (`?NaturalNumbers?succ n) (`?NaturalNumbers?succ m) ≐ le_dec n m  ❙
+❚
\ No newline at end of file

source/calculus/FiniteSequences.mmt

@@ -3,45 +3,14 @@ namespace  http://mathhub.info/MitM/smglom ❚
 
 import base http://mathhub.info/MitM/Foundation ❚
 import arith http://mathhub.info/MitM/smglom/arithmetics ❚
+import sigma http://gl.mathhub.info/MMT/LFX/Sigma ❚
 
 
 
 theory FinSequences : base:?Logic =
 	include arith:?NaturalArithmetics ❙
+	include sigma:?LFSigma ❙
+	include base:?OptionType ❙
 
-	finiteSequence : ℕ ⟶ type ⟶ type ❘= [n : ℕ , A] {x : ℕ}  ⊦  1 ≤ x ⟶ ⊦ x ≤ n ⟶ A ❘# finSeq 1 2 ❙
-
-❚
-
-
-
-theory FinSeqProps : base:?Logic =
-    include arith:?RealArithmetics ❙
-    include ?FinSequences ❙
-    /T A disjoint ❙
-
-	prop_disjointFinSeq : {n : ℕ , A : type} finSeq n A ⟶ bool ❘= [n,A,fs]  ∀[x] ∀[y] ∀[hx1] ∀[hx2] ∀[hy1] ∀[hy2]  y ≐ x ∨ fs x hx1 hx2  ≠ fs y hy1 hy2❙
-
-    prop_ascendingfn : {n : ℕ} finSeq n ℝ ⟶ bool ❘ = [n,fsq] ∀[x] ∀[y] ∀[hx1] ∀[hx2]  ∀[hy1 ] ∀[hy2]  x ≤ y ⇒  arith?RealArithmetics?leq (fsq x hx1 hx2) (fsq y hy1 hy2)  ❘# ascending 2 ❙
-    prop_strictly_ascendingfn : {n : ℕ} finSeq n ℝ ⟶ bool ❘ = [n,fsq] ∀[x] ∀[y] ∀[hx1] ∀[hx2]  ∀[hy1 ] ∀[hy2]  x ≤ y ⇒  arith?RealArithmetics?lessthan (fsq x hx1 hx2) (fsq y hy1 hy2)  ❘# strictly_ascending 2 ❙
-
-❚
-
-theory FinSeqFunctions : base:?InductiveTypes =
-    include ?FinSequences ❙
-    include arith:?INatProps❙
-
-    finiteSequenceMap : {A : type} {B : type} {n : ℕ} finSeq n A ⟶  (A ⟶ B) ⟶ finSeq n B ❘= [A , B , n , fn , mp]  [a ,b ,c] mp (fn a b c)  ❘ # finSeqMap 4 5 ❙
-
-
-    incIf : {A : type} {b : type} ℕ ⟶ ℕ ⟶ ( ℕ ⟶ A) ⟶ A❙
-
-    // helper for finiteSequenceFoldLeft ❙
-    finiteSequenceFoldLeftLoop : {A : type}{B : type}{n : ℕ}{m : ℕ} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘ = [A , B , n , m , f , start , fs] incIf  ❙
-
-    finiteSequenceFoldLeft : {A : type}{B : type} {n : ℕ} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘ # finSeqFoldL 1 2 3 4 5 6 ❙
-    finiteSequenceFoldLeftBZ : {A : type}{B : type}{f : A ⟶ B ⟶ A}{start : A}{fs : finSeq 0 B}  ⊦ finiteSequenceFoldLeft A B 0 f start fs ≐ start❙
-//    finiteSequenceFoldLeftB : {A : type}{B : type}{n : ℕ}{f : A ⟶ B ⟶ A}{start : A}{fs : finSeq n B}  ⊦ finSeqFoldL f start fs ≐ start❙
-
-
+	finiteSequence : ℕ ⟶ type ⟶  type ❘ = [n , A] Σ x : nat ⟶ Option A . ∀ ❙
 ❚

source/calculus/FiniteSequences_alt.mmt

+namespace  http://mathhub.info/MitM/smglom ❚
+
+
+import base http://mathhub.info/MitM/Foundation ❚
+import arith http://mathhub.info/MitM/smglom/arithmetics ❚
+import copro http://gl.mathhub.info/MMT/LFX/Coproducts ❚
+
+
+
+theory FinSequences : base:?Logic =
+	include arith:?NaturalArithmetics ❙
+
+	finiteSequence : ℕ ⟶ type ⟶ type ❘= [n : ℕ , A] {x : ℕ}  ⊦  1 ≤ x ⟶ ⊦ x ≤ n ⟶ A ❘# finSeq 1 2 ❙
+
+❚
+
+theory FinSequencesOption : base:?Logic =
+❚
+
+
+
+theory FinSeqProps : base:?Logic =
+    include arith:?RealArithmetics ❙
+    include ?FinSequences ❙
+    /T A disjoint ❙
+
+	prop_disjointFinSeq : {n : ℕ , A : type} finSeq n A ⟶ bool ❘= [n,A,fs]  ∀[x] ∀[y] ∀[hx1] ∀[hx2] ∀[hy1] ∀[hy2]  y ≐ x ∨ fs x hx1 hx2  ≠ fs y hy1 hy2❙
+
+    prop_ascendingfn : {n : ℕ} finSeq n ℝ ⟶ bool ❘ = [n,fsq] ∀[x] ∀[y] ∀[hx1] ∀[hx2]  ∀[hy1 ] ∀[hy2]  x ≤ y ⇒  arith?RealArithmetics?leq (fsq x hx1 hx2) (fsq y hy1 hy2)  ❘# ascending 2 ❙
+    prop_strictly_ascendingfn : {n : ℕ} finSeq n ℝ ⟶ bool ❘ = [n,fsq] ∀[x] ∀[y] ∀[hx1] ∀[hx2]  ∀[hy1 ] ∀[hy2]  x ≤ y ⇒  arith?RealArithmetics?lessthan (fsq x hx1 hx2) (fsq y hy1 hy2)  ❘# strictly_ascending 2 ❙
+
+❚
+
+theory FinSeqFunctions : base:?InductiveTypes =
+    include ?FinSequences ❙
+    include arith:?INatProps❙
+    include http://gl.mathhub.info/MMT/LFX/Coproducts?LFCoprod ❙
+
+    finiteSequenceMap : {A : type} {B : type} {n : ℕ} finSeq n A ⟶  (A ⟶ B) ⟶ finSeq n B ❘= [A , B , n , fn , mp]  [a ,b ,c] mp (fn a b c)  ❘ # finSeqMap 4 5 ❙
+
+
+
+
+    // helper for finiteSequenceFoldLeft ❙
+    finiteSequenceFoldLeftLoop : {A : type}{B : type}{n : ℕ}{m : ℕ} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘ = [A , B , n , m , f , start , fs] incIf  ❙
+
+    finiteSequenceFoldLeft : {A : type}{B : type} {n : ℕ} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘ # finSeqFoldL 1 2 3 4 5 6 ❙
+    finiteSequenceFoldLeftBZ : {A : type}{B : type}{f : A ⟶ B ⟶ A}{start : A}{fs : finSeq 0 B}  ⊦ finiteSequenceFoldLeft A B 0 f start fs ≐ start❙
+//    finiteSequenceFoldLeftB : {A : type}{B : type}{n : ℕ}{f : A ⟶ B ⟶ A}{start : A}{fs : finSeq n B}  ⊦ finSeqFoldL f start fs ≐ start❙
+
+
+❚