Commit 0890731c by Sven Wille

### redid finsequences with the "normal" natural numbers instead of the inductive ones

parent f3f5797d
 ... ... @@ -89,11 +89,12 @@ theory NaturalArithmetics : base:?Logic = // natToBetween : {from : ℕ}{to : ℕ} {v : ℕ } ⊦ from ≤ v ∧ v ≤ to ⟶ between from to ❘= [v,h] v❙ ❚ // don't use the inductive natural numbers! Inductive types currently aren't very userfriendly ❚ theory InductiveNaturalNumbers : base:?InductiveTypes = induct Nats ()❘ = INat : type ❙ Zero : INat ❙ Zero : INat ❘# Zero ❙ Suc : INat ⟶ INat ❙ ❚ ... ...
 ... ... @@ -4,12 +4,14 @@ namespace http://mathhub.info/MitM/smglom ❚ import base http://mathhub.info/MitM/Foundation ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ // this file contains a minimal and inclomplete formalization ❚ theory FinSequences : base:?InductiveTypes = include arith:?INatArith ❙ finiteSequence : INat ⟶ type ⟶ type ❘= [n : INat , A] {x : INat} ⊦ leN (Suc Zero) x ⟶ ⊦ (leN x n) ⟶ A ❘# finSeq 1 2 ❙ bla : {B : type} finSeq Zero B ❙ ❚ ... ... @@ -36,19 +38,30 @@ theory FinSeqFunctions : base:?InductiveTypes = include arith:?INatProps❙ finiteSequenceMap : {A : type} {B : type} {n : INat} finSeq n A ⟶ (A ⟶ B) ⟶ finSeq n B ❘= [A , B , n , fn , mp] [a ,b ,c] mp (fn a b c) ❘ # finSeqMap 4 5 ❙ def finiteSequenceFoldR (A : type , B : type , startValue : B , fn : A ⟶ B ⟶ B , n : INat, fs : finSeq n A ) ❘ = // ignore the recursive forldr definiton for the time beeing ❙ // def finiteSequenceFoldR (A : type , B : type , startValue : B , fn : A ⟶ B ⟶ B , n : INat, fs : finSeq n A ) ❘ = finSeqFoldR : {m : INat } ⊦ leN m n ⟶ B ❙ // Zero = [p : ⊦ leN Zero n] startValue ❙ // Suc = [mm][p : ⊦ leN (Suc mm) n] startValue ❙ ❚ // Zero = [A : type][B : type][n : INat][startValue : B][p : ⊦ leN Zero n][fs : finSeq n A][fn : A ⟶ B ⟶ B] startValue ❙ // Suc = [m : INat][A : type][B : type][n : INat][startValue : B][p : ⊦ leN Zero n][fs : finSeq n A][fn : A ⟶ B ⟶ B] startValue ❙ // Suc = [m][A][B][n][startValue][h][fs][fn] fn (fs (Suc m) (lemma_One_le_Suc m) h) startValue ❙ // bla : {A : type} {n : INat} {m : INat} ⊦ leN (Suc Zero ) m ⟶ ⊦ leN m n ⟶ finSeq n A ⟶ A ❘ = [A , n , m , p , p0 , fs] fs m p p0 ❙ // helper for finSeqFodlL ❙ // finSeqFoldLRec ❙ // finSeqFoldLRec : {A : type} {B : type}{n : INat}{m : INat} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘ ❙ // finSeqFoldLeft : {A : type} {B : type}{n : INat} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘# finSeqFoldL 4 5 6❙ // finSeqFoldLBZero : {A : type}{B : type}{f : A ⟶ B ⟶ A}{start : A}{fs : finSeq Zero B} ⊦ finSeqFoldLeft A B Zero f start fs ≐ start ❙ // finSeqFoldLB : {A : type}{B : type}{n : INat}(f : A ⟶ B ⟶ A)(start : A){fs : finSeq n A} ⊦ finSeqFoldL f start fs ≐ ❙ ❚ theory FinSeqProd : base:?Logic = finSeqCIntervalProd = [n : INat] [fs : finSeq n type_ci] vector () ℝ ❙ // finSeqCIntervalProd = [n : INat] [fs : finSeq n type_ci] vector () ℝ ❙ ❚
 namespace http://mathhub.info/MitM/smglom ❚ import base http://mathhub.info/MitM/Foundation ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ theory FinSequences : base:?Logic = include arith:?NaturalArithmetics ❙ 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 ❙ // 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] if ❙ 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❙ ❚
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!