Commit ec870dd0 authored by SuperDuckDuck's avatar SuperDuckDuck

removed junk files

parent 0fab84f6
namespace http://mathhub.info/MitM/smglom/Lists ❚
import base http://mathhub.info/MitM/Foundation ❚
theory Lists : base:?Logic =
\ No newline at end of file
namespace http://mathhub.info/MitM/smglom/Lists ❚
import fnd http://mathhub.info/MitM/Foundation ❚
import top http://mathhub.info/MitM/interfaces ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
import sets http://mathhub.info/MitM/smglom/sets ❚
theory Lists : fnd:?Lists =
include fnd:?OptionType ❙
// include top:/Logic?SortedFull ❙
include sets:?relations ❙
include arith:?natarith ❙
include sets:?set ❙
include http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma ❙
nonempty_list : type → type ❘ = [A:type] ⟨ list A | ([x] ⊦ (x ≠ nil A))⟩  # nonempty_list 1 ❙
head: {A} list A → A ❘ # head 2 ❙
tail: {A} nonempty_list A → list A ❘ # tail 2 ❙
concat: {A} list A → list A → list A ❘ # concat 2 3 ❙
reverse: {A} list A → list A ❘ # reverse 2 ❙
length: {A} list A → ℕ ❘ # length 2 ❙
member: {A} A → list A → bool ❘ # member 2 3 ❙
nth: {A} list A → ℕ → A ❘ # nth 2 3 ❙
// remove an element from a list ❙
remove: {A} A → list A → list A ❘ # remove 2 3 ❙
// return the last element of a list; return a default value if the list is empty ❙
last: {A} list A → A → A ❘ # last 2 3 ❙
// remove the last element of a list; does not change an empty list ❙
remove_last: {A} list A → list A ❘ # remove_last 2 ❙
// count the occurrences of an element in a list ❙
count: {A} list A → A → ℕ ❘ # count 2 3 ❙
// concatenate a list of lists ❙
concat_list: {A} list (list A) → list A ❘ # concat_list 2 ❙
// apply a function to each element of a list and concatenate the output ❙
flat_map: {A,B} (A → (list B)) → list A → list B ❘ # flat_map 3 4 ❙
// the set of sequences of elts of y indexed by elts of x, sorted in lexicographic order;
as a set it is the same as the power set ❙
list_power: {A,B} list A → list B → list (list A × B) ❘ # list_power 3 4 ❙
// check whether there is an element of a list satisfying the boolean function ❙
exists: {A} (A → bool) → list A → bool ❘ # exists 2 3 ❙
// check whether all elements of list satisfy the boolean function ❙
forall: {A} (A → bool) → list A → bool ❘ # forall 2 3 ❙
// check whether all elements of two lists are pairwise related according to a relation ❙
forall2: {A,B} relation A B → list A → list B → bool ❘ # forall2 2 3 4 ❙
// check whether all possible ordered pairs of a list are related according to a relation ❙
forall_pairs: {A} relation A A → list A → bool ❘ # forall_pairs 2 3 ❙
// check whether the ordered pairs which have the frontal elements as the first components
of a list are related according to a relation ❙
forall_ordpairs: {A} relation A A → list A → bool ❘ # forall_ordpairs 2 3 ❙
// check whether certain element satisfying the boolean function exists in a list ❙
find: {A} (A → bool) → list A → Option A ❘ # find 2 3 ❙
// the list of elements satisfying the boolean function is the first component ❙
partition: {A} (A → bool) → list A → list A × list A ❘ # partition 2 3 ❙
// split a list of doubletons into a doubleton of lists ❙
split: {A,B} list (A × B) → list A × list B ❘ # split 3 ❙
// combine two lists into one ❙
combine: {A,B} list A → list B → list (A × B) ❘ # combine 3 4 ❙
// return a list of all possible pairs ❙
list_prod: {A,B} list A → list B → list (A × B) ❘ # list_prod 3 4 ❙
// use length as an order on lists ❙
shorter_than: {A} list A → list A → bool ❘ # shorter_than 2 3 ❙
// set inclusion on lists ❙
in: {A} list A → list A → bool ❘ # 2 in 3 ❙
// first n elements ❙
firstn: {A} ℕ → list A → list A ❘ # firstn 2 3 ❙
// complement of first_n ❙
skipn: {A} ℕ → list A → list A ❘ # skipn 2 3 ❙
// check whether there are duplicates in a list ❙
no_duplicates: {A} list A → bool ❘ # no_dup 2 ❙
// remove duplicates of existing elements ❙
remove_duplicates: {A} list A → list A ❘ # remove_dup 2 ❙
// generate a natural number sequence given a starting point (2) and length (3) ❙
nat_sequence: {A:type} ℕ → ℕ → list ℕ ❘ # nat_seq 2 3 ❙
list_comprehension: {A:type} (A → bool) → list A ❘ # list_comprehension 2 ❙
filter: {A:type} (A → bool) → list A → list A ❘ # filter 2 3 ❙
fold_right: {A:type,B:type} (A → B → B) → B → list A → B ❘ # fold_right 3 4 5 ❙
fold_left: {A:type,B:type} (A → B → B) → B → list A → B ❘ # fold_left 3 4 5 ❙
map: {A,B} (A → B) → list A → list B ❘ # map 3 4 ❙
//Weirdly, doesn't typecheck
//concat_def: {A} ⊦ ∀ [l:list A] ∀ [m:list A] (concat l m) ≐ (fold_left cons m l) ❙
filter_def: ⊦ {A} ∀ [l:list A] ∀ [p:A → bool] (filter p l) ≐ (list_comprehension ([a:A] ((p a) ∧ (member a l)))) ❙
fold_left_def: ⊦ {A:type,B:type} ∀ [f:A → B → B] ∀ [b:B] ∀ [l:list A] fold_left f b l ≐ fold_right f b (reverse l) ❙
map_def: ⊦ {A:type,B:type} ∀ [f:A → B] ∀ [l:list A] map f l ≐ (list_comprehension ([b:B] (forall ([a:A] f a ≐ b) l))) ❙
//The next line doesn't typecheck, looks like a bug in the definition of nil (getting same issue after replacing l with nil in concat_def)
map_def2: ⊦ {A:type,B:type} ∀ [f:A → B] ∀ [l:list A] map f l ≐ fold_left ([a:A,m:list B] ((f a) , m)) nil l ❙
exists_axiom: ⊦ {A} ∀ [l:list A] ∀ [p:A → bool] exists p l ≐ ¬ forall ([a:A] ¬ p a) l ❙
forall_axiom: ⊦ {A} ∀ [l:list A] ∀ [p:A → bool] forall p l ≐ ¬ exists ([a:A] ¬ p a) l ❙
theory finite_sequences : fnd:?Logic =
include sets:?relations ❙
include arith:?natarith ❙
include sets:?set ❙
//include top:?TypingJudgments ❙
first_nats: {n:ℕ} ⟨set ℕ | ([s] ⊦ ∀ [x:ℕ] inset ℕ x s ≐ lessthan x n)⟩ ❘ # upto 1 ❙
fin_seq: type → type ❘ # fseq 1 ❙
fseq_nil: type → type ❘ # fseq_nil 1 ❙
single: {A} A → fseq A ❘ # single 2 ❙
concat: {A} fseq A → fseq A → fseq A ❘ # fseq_concat 2 3 ❙
fseq_cons: {A} A → fseq A → fseq A ❘ = [A:type,a:A,seq:fseq A] fseq_concat (single a) seq ❘ # fseq_cons 2 3 ❙
term: {A} A → fseq A → bool ❘ # term 2 3 ❙
length: {A} fseq A → ℕ ❘ # fseq_length 2 ❙
take: {A} ℕ → fseq A → fseq A ❘ # take 2 3 ❙
indexset: {A} fseq A → set ℕ  = [A,s] upto (fseq_length s) ❘ # indexset 2 ❙
finite_set_sequence: {A} (set A) → fseq A ❘ # fset_seq 2 ❙
//index: {A:type,s:fseq A} ⟨ℕ | ([x] ⊦ inset ℕ x (upto (length s)))⟩ → A ❘ # index 2 3 ❙
head: {A} fseq A → A ❘ # head 2 ❙
tail: {A} fseq A → fseq A ❘ # tail 2 ❙
reverse: {A} fseq A → fseq A ❘ # reverse 2 ❙
filter: {A} (A → bool) → fseq A → fseq A ❘ # filter 2 3 ❙
fseq_fold_right: {A:type,B:type} (A → B → B) → B → fseq A → B ❘ # fseq_fold_right 3 4 5 ❙
fseq_fold_left: {A:type,B:type} (A → B → B) → B → fseq A → B ❘ # fseq_fold_left 3 4 5 ❙
map: {A,B} (A → B) → fseq A → fseq B ❘ # map 3 4 ❙
any: {A} fseq A → (A → bool) → bool ❘ # any 2 3 ❙
some: {A} fseq A → (A → bool) → bool ❘ # some 2 3 ❙
//This doen't work as we are making a claim about a type, thus the typechecker actually needs a proof
//of the statement, which wasn't given in a definition, thus can't be infered
//Therefore, typechecking fails. Only possible fix is in adapting the definition of fseq to some weird subtype
//Leaving this for documentation purpose
//
////For now, this should be removed as soon as the Functions_are_Relations lemma is in place
////This is not referenced to in alignments, but used in Lists/finite_sequences
//restriction_fct: {A,B} function A B → {C} function C B ❘ # 3 restrict_fct 4 ❙
//fin_seq_def: ⊦ {A:type} ∀ [seq:fseq A] ∃ [f:ℕ → A] seq ≐ f | ⟨ ℕ | ([x] ⊦ x in (upto (length seq)))⟩ ❙
theory lists_as_sequences : fnd:?Logic =
include ?Lists ❙
include ?finite_sequences ❙
//list_to_sequence: {A} list A → fseq A ❘ = [A,l] fold_left ([a,b] fseq_cons (single a) b) fseq_nil l ❘ # list_to_sequence 2 ❙
namespace http://mathhub.info/MitM/smglom/Lists ❚
import base http://mathhub.info/MitM/Foundation ❚
import top http://mathhub.info/MitM/interfaces ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
import sets http://mathhub.info/MitM/smglom/sets ❚
theory Lists : base:?Lists =
include base:?OptionType ❙
// include top:/Logic?SortedFull ❙
// include sets:?relations ❙
// include arith:?natarith ❙
// include sets:?set ❙
include http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma ❙
nonempty_list : type ⟶ type ❘ = [A:type] ⟨ list A | ([x] ⊦ (x ≠ nil A))⟩  # nonempty_list 1 ❙
head: {A} list A ⟶ A ❘ # head 2 ❙
tail: {A} nonempty_list A ⟶ list A ❘ # tail 2 ❙
concat: {A} list A ⟶ list A ⟶ list A ❘ # concat 2 3 ❙
reverse: {A} list A ⟶ list A ❘ # reverse 2 ❙
length: {A} list A ⟶ ℕ ❘ # length 2 ❙
member: {A} A ⟶ list A ⟶ bool ❘ # member 2 3 ❙
nth: {A} list A ⟶ ℕ ⟶ A ❘ # nth 2 3 ❙
// remove an element from a list ❙
remove: {A} A ⟶ list A ⟶ list A ❘ # remove 2 3 ❙
// return the last element of a list; return a default value if the list is empty ❙
last: {A} list A ⟶ A ⟶ A ❘ # last 2 3 ❙
// remove the last element of a list; does not change an empty list ❙
remove_last: {A} list A ⟶ list A ❘ # remove_last 2 ❙
// count the occurrences of an element in a list ❙
count: {A} list A ⟶ A ⟶ ℕ ❘ # count 2 3 ❙
// concatenate a list of lists ❙
concat_list: {A} list (list A) ⟶ list A ❘ # concat_list 2 ❙
// apply a function to each element of a list and concatenate the output ❙
flat_map: {A,B} (A ⟶ (list B)) ⟶ list A ⟶ list B ❘ # flat_map 3 4 ❙
// the set of sequences of elts of y indexed by elts of x, sorted in lexicographic order;
as a set it is the same as the power set ❙
list_power: {A,B} list A ⟶ list B ⟶ list (list A × B) ❘ # list_power 3 4 ❙
// check whether there is an element of a list satisfying the boolean function ❙
exists: {A} (A ⟶ bool) ⟶ list A ⟶ bool ❘ # exists 2 3 ❙
// check whether all elements of list satisfy the boolean function ❙
forall: {A} (A ⟶ bool) ⟶ list A ⟶ bool ❘ # forall 2 3 ❙
// check whether all elements of two lists are pairwise related according to a relation ❙
forall2: {A,B} relation A B ⟶ list A ⟶ list B ⟶ bool ❘ # forall2 2 3 4 ❙
// check whether all possible ordered pairs of a list are related according to a relation ❙
forall_pairs: {A} relation A A ⟶ list A ⟶ bool ❘ # forall_pairs 2 3 ❙
// check whether the ordered pairs which have the frontal elements as the first components
of a list are related according to a relation ❙
forall_ordpairs: {A} relation A A ⟶ list A ⟶ bool ❘ # forall_ordpairs 2 3 ❙
// check whether certain element satisfying the boolean function exists in a list ❙
find: {A} (A ⟶ bool) ⟶ list A ⟶ Option A ❘ # find 2 3 ❙
// the list of elements satisfying the boolean function is the first component ❙
partition: {A} (A ⟶ bool) ⟶ list A ⟶ list A × list A ❘ # partition 2 3 ❙
// split a list of doubletons into a doubleton of lists ❙
split: {A,B} list (A × B) ⟶ list A × list B ❘ # split 3 ❙
// combine two lists into one ❙
combine: {A,B} list A ⟶ list B ⟶ list (A × B) ❘ # combine 3 4 ❙
// return a list of all possible pairs ❙
list_prod: {A,B} list A ⟶ list B ⟶ list (A × B) ❘ # list_prod 3 4 ❙
// use length as an order on lists ❙
shorter_than: {A} list A ⟶ list A ⟶ bool ❘ # shorter_than 2 3 ❙
// set inclusion on lists ❙
in: {A} list A ⟶ list A ⟶ bool ❘ # 2 in 3 ❙
// first n elements ❙
firstn: {A} ℕ ⟶ list A ⟶ list A ❘ # firstn 2 3 ❙
// complement of first_n ❙
skipn: {A} ℕ ⟶ list A ⟶ list A ❘ # skipn 2 3 ❙
// check whether there are duplicates in a list ❙
no_duplicates: {A} list A ⟶ bool ❘ # no_dup 2 ❙
// remove duplicates of existing elements ❙
remove_duplicates: {A} list A ⟶ list A ❘ # remove_dup 2 ❙
// generate a natural number sequence given a starting point (2) and length (3) ❙
nat_sequence: {A:type} ℕ ⟶ ℕ ⟶ list ℕ ❘ # nat_seq 2 3 ❙
list_comprehension: {A:type} (A ⟶ bool) ⟶ list A ❘ # list_comprehension 2 ❙
filter: {A:type} (A ⟶ bool) ⟶ list A ⟶ list A ❘ # filter 2 3 ❙
fold_right: {A:type,B:type} (A ⟶ B ⟶ B) ⟶ B ⟶ list A ⟶ B ❘ # fold_right 3 4 5 ❙
fold_left: {A:type,B:type} (A ⟶ B ⟶ B) ⟶ B ⟶ list A ⟶ B ❘ # fold_left 3 4 5 ❙
map: {A,B} (A ⟶ B) ⟶ list A ⟶ list B ❘ # map 3 4 ❙
//Weirdly, doesn't typecheck
//concat_def: {A} ⊦ ∀ [l:list A] ∀ [m:list A] (concat l m) ≐ (fold_left cons m l) ❙
filter_def: ⊦ {A} ∀ [l:list A] ∀ [p:A ⟶ bool] (filter p l) ≐ (list_comprehension ([a:A] ((p a) ∧ (member a l)))) ❙
fold_left_def: ⊦ {A:type,B:type} ∀ [f:A ⟶ B ⟶ B] ∀ [b:B] ∀ [l:list A] fold_left f b l ≐ fold_right f b (reverse l) ❙
map_def: ⊦ {A:type,B:type} ∀ [f:A ⟶ B] ∀ [l:list A] map f l ≐ (list_comprehension ([b:B] (forall ([a:A] f a ≐ b) l))) ❙
//The next line doesn't typecheck, looks like a bug in the definition of nil (getting same issue after replacing l with nil in concat_def)
map_def2: ⊦ {A:type,B:type} ∀ [f:A ⟶ B] ∀ [l:list A] map f l ≐ fold_left ([a:A,m:list B] ((f a) , m)) nil l ❙
exists_axiom: ⊦ {A} ∀ [l:list A] ∀ [p:A ⟶ bool] exists p l ≐ ¬ forall ([a:A] ¬ p a) l ❙
forall_axiom: ⊦ {A} ∀ [l:list A] ∀ [p:A ⟶ bool] forall p l ≐ ¬ exists ([a:A] ¬ p a) l ❙
theory finite_sequences : base:?Logic =
// include sets:?relations ❙
// include arith:?natarith ❙
// include sets:?set ❙
// include top:?TypingJudgments ❙
first_nats: {n:ℕ} ⟨set ℕ | ([s] ⊦ ∀ [x:ℕ] inset ℕ x s ≐ lessthan x n)⟩ ❘ # upto 1 ❙
fin_seq: type ⟶ type ❘ # fseq 1 ❙
fseq_nil: type ⟶ type ❘ # fseq_nil 1 ❙
single: {A} A ⟶ fseq A ❘ # single 2 ❙
concat: {A} fseq A ⟶ fseq A ⟶ fseq A ❘ # fseq_concat 2 3 ❙
fseq_cons: {A} A ⟶ fseq A ⟶ fseq A ❘ = [A:type,a:A,seq:fseq A] fseq_concat (single a) seq ❘ # fseq_cons 2 3 ❙
term: {A} A ⟶ fseq A ⟶ bool ❘ # term 2 3 ❙
length: {A} fseq A ⟶ ℕ ❘ # fseq_length 2 ❙
take: {A} ℕ ⟶ fseq A ⟶ fseq A ❘ # take 2 3 ❙
indexset: {A} fseq A ⟶ set ℕ  = [A,s] upto (fseq_length s) ❘ # indexset 2 ❙
finite_set_sequence: {A} (set A) ⟶ fseq A ❘ # fset_seq 2 ❙
//index: {A:type,s:fseq A} ⟨ℕ | ([x] ⊦ inset ℕ x (upto (length s)))⟩ ⟶ A ❘ # index 2 3 ❙
head: {A} fseq A ⟶ A ❘ # head 2 ❙
tail: {A} fseq A ⟶ fseq A ❘ # tail 2 ❙
reverse: {A} fseq A ⟶ fseq A ❘ # reverse 2 ❙
filter: {A} (A ⟶ bool) ⟶ fseq A ⟶ fseq A ❘ # filter 2 3 ❙
fseq_fold_right: {A:type,B:type} (A ⟶ B ⟶ B) ⟶ B ⟶ fseq A ⟶ B ❘ # fseq_fold_right 3 4 5 ❙
fseq_fold_left: {A:type,B:type} (A ⟶ B ⟶ B) ⟶ B ⟶ fseq A ⟶ B ❘ # fseq_fold_left 3 4 5 ❙
map: {A,B} (A ⟶ B) ⟶ fseq A ⟶ fseq B ❘ # map 3 4 ❙
any: {A} fseq A ⟶ (A ⟶ bool) ⟶ bool ❘ # any 2 3 ❙
some: {A} fseq A ⟶ (A ⟶ bool) ⟶ bool ❘ # some 2 3 ❙
//This doen't work as we are making a claim about a type, thus the typechecker actually needs a proof
//of the statement, which wasn't given in a definition, thus can't be infered
//Therefore, typechecking fails. Only possible fix is in adapting the definition of fseq to some weird subtype
//Leaving this for documentation purpose
//
////For now, this should be removed as soon as the Functions_are_Relations lemma is in place
////This is not referenced to in alignments, but used in Lists/finite_sequences
//restriction_fct: {A,B} function A B ⟶ {C} function C B ❘ # 3 restrict_fct 4 ❙
//fin_seq_def: ⊦ {A:type} ∀ [seq:fseq A] ∃ [f:ℕ ⟶ A] seq ≐ f | ⟨ ℕ | ([x] ⊦ x in (upto (length seq)))⟩ ❙
theory lists_as_sequences : fnd:?Logic =
include ?Lists ❙
include ?finite_sequences ❙
//list_to_sequence: {A} list A ⟶ fseq A ❘ = [A,l] fold_left ([a,b] fseq_cons (single a) b) fseq_nil l ❘ # list_to_sequence 2 ❙
namespace http://mathhub.info/MitM/smglom/arithmetics ❚
import base http://mathhub.info/MitM/Foundation ❚
// used as a return type in for the indicator function in indicatorFunction.mmt❚
theory ZeroOne : base:?Logic =
include ?NaturalNumbers ❙
zeroOne : type ❘= ⟨ ℕ | [x] ⊦ x ≐ 1 ∨ x ≐ 0⟩ ❙
\ No newline at end of file
namespace http://mathhub.info/MitM/smglom/misc ❚
import fnd http://mathhub.info/MitM/Foundation ❚
import base http://mathhub.info/MitM/Foundation ❚
// theory comparison : fnd:?Logic =
comparison : type ❘ # comparison ❙
greater_than : comparison ❘ # gt ❙
equal : comparison ❘ # eq ❙
less_than : comparison ❘ # lt ❙
opposite : comparison ⟶ comparison ❘ # opposite 1 ❙
theory option : base:?Logic =
option : type ⟶ type ❘ # option 1 ❙
some : {A} A ⟶ option A ❘ # some 2 ❙
none : {A} option A ❘ # none ❙
// none A is mapped to none B; some A a is mapped to some B (f a) ❙
option_map : {A,B} (A ⟶ B) ⟶ option A ⟶ option B ❘ # option_map 3 4 ❙
// theory disjoint_sum : fnd:?Logic =
disjoint_sum : type ⟶ type ⟶ type ❘ # 1 + 2 ❙
inj1 : {A,B} A ⟶ A + B ❘ # inj1 3 ❙
inj2 : {A,B} B ⟶ A + B ❘ # inj2 3 ❙
// a sample interface for product type; feel free to remove or edit this ❚
theory product : base:?Logic =
// include fnd:?NatLiterals ❙
bla : (type × type) ❙
product : type ⟶ type ⟶ type ❘ # 1 × 2 ❙
proj1 : {A,B} A × B ⟶ A ❘ # proj1 3 ❙
proj2 : {A,B} A × B ⟶ B ❘ # proj2 3 ❙
prod_curry : {A,B,C : type} (A ⟶ B ⟶ C) ⟶ (A × B) ⟶ C ❘ # curry 4 5 ❙
prod_uncurry : {A,B,C : type} (A × B ⟶ C) ⟶ A ⟶ B ⟶ C ❘ # uncurry 4 5 6 ❙
// power : ℕ ⟶ type ⟶ type ❘ # 2 ^ 1 ❙
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment