namespace http://mathhub.info/MitM/Foundation ❚

import rules scala://rules.mitm.mmt.kwarc.info ❚
import lf scala://lf.mmt.kwarc.info ❚
import lfx scala://LFX.mmt.kwarc.info ❚

fixmeta http://cds.omdoc.org/mmt?mmt ❚

theory Metadata =
	constructorargument ❙
❚

/T We define a formal language for basic mathematical objects in LF. ❚

theory Subtyping =
	 include ☞http://gl.mathhub.info/MMT/LFX/Subtyping?LFSubtyped ❙
❚

/T First, some logic. ❚

                                               
theory Logic : http://gl.mathhub.info/MMT/LFX/TypedHierarchy?LFHierarchy =
	 include ☞http://gl.mathhub.info/MMT/LFX/Records?LFRecords ❙
	 include ☞http://cds.omdoc.org/urtheories?Ded ❙
	 include ☞http://gl.mathhub.info/MMT/LFX/Subtyping?LFWithVariance ❙
	 
	 // rule rules?ApplyRule ❙
	 
	 /T the type of booleans, i.e., all formulas are represented as terms of LF-type $prop$ ❙
	 // bool : type ❘ // = BOOL ❙
	 prop : type ❘ @ bool ❘ = BOOL ❙
	 
	 /T one LF-type for each formula holding its proofs                 
	 For example, the LF type ⊦ 0 ≐ 1 is empty because that formula has no proofs.
	 Axioms are declared as constants of the corresponding type, e.g., a constant of type $⊦ true$ for the axiom of truth.❙
	 ded : prop ⟶ type ❘ # ⊦ 1 prec -500 ❘ role Judgment ❘ = DED ❙
	 ImplicitProof : {A} ⊦ A ❘ # ImplicitProof 1 ❙
	 rule lf?TermIrrelevanceRule (ded) ([A : prop] ImplicitProof A) ❙
	 
	 /T Equality on terms. The type A is left implicit and can be inferred by MMT ❙
	 eq : {A:𝒰 100} A ⟶ A ⟶ bool ❘ # 2 ≐ 3 prec -5 ❘ role Eq ❘ // = EQUAL ❙
	 
	 
	 // coercion : {A : type, P : A ⟶ prop,a} ⊦ P a ⟶ ⟨ A | ([x] ⊦ P x) ⟩ ❘ # coerce 3 %I4❙
	 // coercion_theorem : {A : type,P : A ⟶ prop,a,p : ⊦ P a} ⊦ eq ⟨ A | ([x] ⊦ P x) ⟩ (coercion A P a p) a ❙
	 
	 rule rules?BooleanLiterals ❙
	 
	 // false_is_FALSE : ded (FALSE ≐ false) ❙
	 // true_is_TRUE : ded (TRUE ≐ true) ❙
	 
	 not  : bool ⟶ bool ❘ # ¬ 1 prec -100 ❙
	 neq : {A: 𝒰 100} A ⟶ A ⟶ prop ❘ # 2 ≠ 3 prec -5 ❘ = [A,a,b] ¬ (a ≐ b) ❙

	 and  : bool ⟶ bool ⟶ bool❘# 1 ∧ 2 prec -110 ❙
	 
	 or : bool ⟶ bool ⟶ bool ❘# 1 ∨ 2 prec -120 ❘ // = [A,B] ¬ (¬A ∧ ¬ B) ❙
	 implies : bool ⟶ bool ⟶ bool ❘# 1 ⇒ 2 prec -130 ❘ // = [A,B] B ∨ ¬A ❙
	 iff : bool ⟶ bool ⟶ bool ❘ # 1 ⇔ 2 prec -140 ❘// = [A,B] (A ⇒ B) ∧ (B ⇒ A) ❙
   
	 forall : {A : 𝒰 100} (A ⟶ bool) ⟶ bool ❘ # ∀ 2 prec -100❙
	 exists : {A : 𝒰 100} (A ⟶ bool) ⟶ bool ❘ # ∃ 2 prec -100 ❘// = [A,f] ¬ ∀ [x:A] ¬ f x ❙
	 unique : {A : 𝒰 100} (A ⟶ bool) ⟶ A ⟶ bool ❘ = [A,P,x] ∀ [y:A] P y ⇒ y ≐ x ❘ # unique 2 3 ❙
	 exists_unique : {A : 𝒰 100} (A ⟶ bool) ⟶ bool ❘ # ∃! 2 prec -101 ❘ = [A,P] ∃ [x] (P x ∧ unique P x) ❙
   
	 /T Equality on types (semantics missing) ❙
	 tpeq : type ⟶ type ⟶ bool ❘ # 1 ≐≐ 2 prec -6 ❘ role Eq ❙	 		
	 
❚
	 
theory NaturalDeduction : ur:?LF =
	 include ?Logic ❙
	 
	 tru_introduction : ⊦ true ❙
	 fals_elimination : {A} ⊦ false ⟶ ⊦ A ❙
	 fals_introduction : {A} ⊦ A ⟶ ⊦ ¬ A ⟶ ⊦ false ❙
	 
	 forall_elim : {A : 𝒰 100, P : A ⟶ bool}⊦ ∀ P ⟶ {x : A}⊦ P x ❘ # forallE 3 4❙
	 forall_introduction : {A : 𝒰 100, P : A ⟶ bool, p : {x : A}⊦P x}⊦ ∀[x] P x ❘ # forallI 3 ❙

	 and_introduction : {A,B} ⊦ A ⟶ ⊦ B ⟶ ⊦ (A ∧ B) ❙
	 and_elim_left : {A,B} ⊦ (A ∧ B) ⟶ ⊦ A ❙
	 and_elim_right : {A,B} ⊦ (A ∧ B) ⟶ ⊦ B ❙
	 
	 not_introduction : {A} (⊦ A ⟶ ⊦ false) ⟶ ⊦ ¬ A ❙
	 not_elim : {A} ⊦ ¬ ¬ A ⟶ ⊦ A ❙

	 tnd : {A} ⊦ A ∨ ¬A ❘ // = [A: bool] not_introduction ([p : ⊦ (¬A ∧ ¬¬A)] fals_introduction (not_elim (and_elim_right p)) (and_elim_left p)) ❙

	/T Some more rules for convenience. ❙

        or_introduction_right :  {A,B} ⊦ A ⟶ ⊦ (A ∨ B) ❘ # orinr 3❙
        or_introduction_left :  {A,B} ⊦ B ⟶ ⊦ (A ∨ B) ❘ # orinl 3❙
        implication_introduction : {A,B} (⊦ A ⟶ ⊦ B) ⟶ ⊦ A ⇒ B ❘ # impli 3❙
        equiv_introduction : {A,B} ⊦ (A ⇒ B) ⟶ ⊦ (B ⇒ A) ⟶ ⊦ (A ⇔ B) ❘ # equivi 3 4❙
        or_elimination : {A,B} ⊦ (A ∨ B) ⟶ (⊦ A ⟶ ⊦ C) ⟶ (⊦ B ⟶ ⊦ C) ⟶ ⊦ C ❘ # orelim 3 4 5❙
        modus_ponens : {A,B} (⊦ A ⇒ B) ⟶ ⊦ A ⟶ ⊦ B ❘ # MP 3 4 ❙
	 
	 /T basic axioms governing Equality. Again, all the type parameters can be left implicit ❙
	 eq_refl : {t:𝒰 100,A: t} ⊦ A ≐ A ❘ # eq_refl 2❙
	 eq_cong : {t : 𝒰 100, s : 𝒰 100, f : t ⟶ s, A : t, B: t}
	 		⊦ A ≐ B ⟶ ⊦ (f A) ≐ (f B) ❘ # eq_cong 3 6❙
	 
❚
	 

/T Now some theories that introduce primitive types and literals for them.
     Because literals must modify the parser, they are supplied as rules that are implemented in a plugin.❚   
   
theory NatLiterals : ur:?LF =
	include ?Logic ❙
	include ?Subtyping ❙
	include ☞http://cds.omdoc.org/urtheories?NatLiterals ❙
	include ☞http://cds.omdoc.org/urtheories?NatRels ❙
	
	nat_lit : type ❘ # ℕ ❘ = NAT ❙
	// rule rules?NatLiterals ❙
	pos_lit : type ❘ = ⟨ n : nat_lit | ⊦ n ≠ 0 ⟩ ❘ # ℕ+ ❙
	rule rules?PosLiterals ❙
	pos_are_nat : pos_lit <* nat_lit ❙
	
	succ_nat_lit : nat_lit ⟶ pos_lit ❙
	rule rules?NatSucc ❙
	// not needed anymore: rule rules?NatSuccInverse ❙
	
	plus_pos_lit : pos_lit ⟶ pos_lit ⟶ pos_lit ❙
	rule rules?PosPlus ❙
	plus_nat_lit : nat_lit ⟶ nat_lit ⟶ nat_lit ❘ = plus ❙
	// rule rules?NatPlus ❙
   	times_pos_lit : pos_lit ⟶ pos_lit ⟶ pos_lit ❙
	rule rules?PosTimes ❙
	times_nat_lit : nat_lit ⟶ nat_lit ⟶ nat_lit ❘= times ❙
	// rule rules?NatTimes ❙
    leq_nat_lit : nat_lit ⟶ nat_lit ⟶ bool ❘ = LEQ ❙
	// rule rules?NatLeq ❙
❚
	
theory IntLiterals : ur:?PLF =
	include ?Logic ❙
	
	int_lit: type ❘ # ℤ ❙
	rule rules?IntegerLiterals ❙
	
	minus_int_lit : int_lit ⟶ int_lit ❙
	rule rules?IntMinus ❙
	plus_int_lit : int_lit ⟶ int_lit ⟶ int_lit ❙
	rule rules?IntPlus ❙
  times_int_lit : int_lit ⟶ int_lit ⟶ int_lit ❙
	rule rules?IntTimes ❙
  leq_int_lit : int_lit ⟶ int_lit ⟶ bool ❙
	rule rules?IntLeq ❙
❚
	
theory RealLiterals : ur:?LF =
	include ?Logic ❙
   
	real_lit: type ❘ # ℝ ❙
	rule rules?RealLiterals ❙
	
	leq_real_lit : real_lit ⟶ real_lit ⟶ bool ❙
   	rule rules?RealLeq ❙
   	minus_real_lit : real_lit ⟶ real_lit  ❘ # - 1 prec 25 ❙
   	rule rules?RealMinus ❙   
   	plus_real_lit : real_lit ⟶ real_lit ⟶ real_lit ❘ # 1 + 2 prec 25 ❙
	rule rules?RealPlus ❙
   	times_real_lit : real_lit ⟶ real_lit ⟶ real_lit ❘ # 1 × 2 prec 20 ❙
	rule rules?RealTimes ❙
	
	
	// square_is_pos : {r : ℝ} ⊦ leq_real_lit 0 (times_real_lit r r) ❙
	sqrt  : ℝ ⟶ ℝ ❙
	rule rules?RealSqrt ❙
❚
     
theory Literals : ur:?LF =
   include ?RealLiterals ❙
   include ?NatLiterals ❙
   include ?IntLiterals ❙
   include ?Subtyping ❙

   ints_are_real : int_lit <* real_lit ❙
   
   nats_are_int : nat_lit <* int_lit ❙
   nats_are_real : nat_lit <* real_lit ❙
   
   pos_are_int : pos_lit <* int_lit ❙
   pos_are_real : pos_lit <* real_lit ❙
   
   // rule rules?NumberLiterals ❙

   // test : ⊦ leq_lit 0 1 ❘ = tru_introduction ❙
   // test2 : ⊦ nat_lit_succ 1 ≐ 2 ❘ = eq_refl 2 ❙
	 
❚
   
theory Trigonometry : ur:?LF =
	include ?RealLiterals ❙
	
	tan   : real_lit ⟶ real_lit    ❙
	sin   : real_lit ⟶ real_lit    ❙
	cos   : real_lit ⟶ real_lit    ❙
	atan   : real_lit ⟶ real_lit    ❙
	asin   : real_lit ⟶ real_lit    ❙
	acos   : real_lit ⟶ real_lit    ❙
	
	rule rules?Tan ❙
	rule rules?Sin ❙
	rule rules?Cos ❙
	rule rules?Atan ❙
	rule rules?Asin ❙
	rule rules?Acos ❙
❚
	 
/T String literals are also needed occasionally, e.g., in the LMFDB.❚
 
theory Strings : ur:?LF =
   include ?Logic❙
   string: type ❙
	 rule rules?StringLiterals ❙
	 concat: string ⟶ string ⟶ string❙
❚

/T Now some more complex types. First lists.❚

theory Lists : ur:?LF =
   include ☞http://gl.mathhub.info/MMT/LFX/Datatypes?LFLists ❙
❚

theory InformalProofs : ur:?LF = 
  include ?Strings ❙
   	 
	proofsketch : {A : prop} string ⟶ ⊦ A ❘ # sketch 2 ❙
	byproof : {A,B} ⊦ A ⟶ ⊦ B ❘ # by 3 ❙
	addproofstep : {A,B,C: prop} ⊦ A ⟶ ⊦ B ⟶ ⊦ B ❘ # 4 and 5 ❙
	trivial : {A : prop} ⊦ A ❘ = [A] sketch "trivial" ❘ # trivial %I1 ❙
❚


/T (Finite) sets ❙
theory Sets : ur:?LF =
   include ?Logic❙
   /T the type operator of sets along with its constructors❙
   set: type ⟶ type ❙
   
   empty: {A} (list A) ❘# ∅ 1❘## ∅ %I1 ❙
   cons: {A} A ⟶ (list A) ⟶ (list A)❘ # 2 , 3 ❙ 
❚

/T Multisets ❙

/T "Finite hybrid sets" (mutlisets with possibly negative mutliplicities) ❙

/T Now vectors, i.e., fixed-length lists.❚

theory Vectors : ur:?PLF =
  include ?Logic❙
	include ?Literals ❙
	
   /T the type operator of vectors (fixed-length lists) over a given type ❙
   vector : 𝒰 100 ⟶ nat_lit ⟶ type ❘ # 1 ^^ 2 prec 32 ❙
   
   zerovec : {t : 𝒰 100} vector t 0 ❙
   vector_prepend : {t: 𝒰 100,n : nat_lit, a : t, b : vector t n} t ^^ (succ_nat_lit n) ❘ # 3 ; 4❙
❚

theory Matrices : ur:?LF =
  include ?Logic❙
	include ?Vectors ❙
	
  /T the type operator of matrices over a given type❙
  matrix : 𝒰 100 ⟶ nat_lit ⟶ nat_lit ⟶ type ❘ = [T,n,m] vector (vector T m) n ❙
❚

theory OptionType : ur:?PLF =
	include ?Logic ❙
	
	Option : 𝒰 100 ⟶ 𝒰 100 ❙
	
	isDefined : {A} Option A ⟶ prop ❘ # isDefined 2❙
	OptionGet : {A, a : Option A} ⊦ isDefined a ⟶ A ❘ # get 2 %I3 ❙
	
	None : {A : 𝒰 100} Option A ❘ # None ❙
	None_is_not_Defined : {A : 𝒰 100} ⊦ isDefined (None A) ≐ false ❙
	Not_None_is_Defined : {A, a : Option A} ⊦ (a ≠ None A) ⟶ ⊦ isDefined a ❙
	Some : {A: 𝒰 100} A ⟶ Option A ❘ # Some 2 ❙
	Some_is_Defined : {A : 𝒰 100}{a:A} ⊦ isDefined (Some a) ❙
	get_some : {A : 𝒰 100}{a:A} ⊦ get (Some a) ≐ a ❙
❚

theory DescriptionOperator : ur:?PLF =
	include ?OptionType ❙
	
	that : {A:𝒰 100,P:A ⟶ bool} ⊦ (∃! P) ⟶  A ❘ # ι 2 %I3 ❙
	that_proof : {A : 𝒰 100, P : A ⟶ bool, p : ⊦ ∃! P} ⊦ P (that A P p) ❙
	
	if_then_else_exists_proof : {A,P,a:A,b:A} ⊦ ∃! [x:A] (P ∧ x ≐ a) ∨ (¬ P ∧ x ≐ b) ❘ # iteep 2 3 4❙
	if_then_else : {A : 𝒰 100, P : bool, a : A, b : A}A ❘ # if 2 then 3 else 4 ❘
		= [A,P,a,b] that A ([x] (P ∧ x ≐ a) ∨ (¬ P ∧ x ≐ b)) (iteep P a b) ❙
	if_then_else_case : {A : 𝒰 100, P : bool, a : A, b : A}A ❘ = [A,P,a,b] if P then a else b ❘ # case 2 ⟹ 3 . 4 prec 2 ❙
	
	if_true : {A : 𝒰 100, P : bool, a : A, b : A, p : ⊦ P} ⊦ (if P then a else b) ≐ a ❘ // = [A,P,a,b,p] _ ❘ ❙
	if_false : {A : 𝒰 100, P : bool, a : A, b : A, p : ⊦ ¬ P } ⊦ (if P then a else b) ≐ b ❘ // = [A,P,a,b,p] _ ❘ ❙
❚

theory ProductTypes : http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma =
	// to have it in the meta-theory ❙                       
❚
theory FiniteTypes : http://gl.mathhub.info/MMT/LFX/Finite?LFFinite = ❚
theory InductiveTypes : http://gl.mathhub.info/MMT/LFX/WTypes?Inductive =
    include ?Logic ❙
❚

theory Sequences =
	include ☞ur:?Sequences ❙
	include ☞ur:?LFS ❙
	include ?Logic ❙
	
	forall_seq : {A: type}{n} (A^n ⟶ prop) ⟶ prop ❘ # ∀n 3 prec -101 ❙
	exists_seq : {A: type}{n} (A^n ⟶ prop) ⟶ prop ❘ # ∃n 3 prec -101 ❘ = [A,n][P] ¬ forall_seq A n [s : A^n] ¬ (P s)❙
❚

/T Finally, a theory that puts everything together (not recommended, because modularity) ❚

theory Math : ur:?PLF =
	include ?Subtyping ❙
	include ?Logic ❙
	include ?NaturalDeduction ❙
	include ?Literals ❙
	include ?Trigonometry ❙
	include ?Strings ❙
	include ?InformalProofs ❙
	include ?Lists ❙
	include ?Vectors ❙
	include ?Matrices ❙
	include ?OptionType ❙
	include ?DescriptionOperator ❙
	include ?ProductTypes ❙
	include ?Sequences ❙
❚