namespace http://cds.omdoc.org/examples ❚

import lfx http://gl.mathhub.info/MMT/LFX/TypedHierarchy ❚
import finite http://gl.mathhub.info/MMT/LFX/Finite ❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚

theory InductiveTests : ?InductivelyDefinedTypes =
	lst: type ⟶ type ❘ = [a] list1/list a ❙
	cns: {a:type} a ⟶ lst a ⟶ lst a ❘ = [a, hd, tl] list1/cons a hd tl ❙

	contraposition: {a: type, b: type, x_a: a, x_b: b, y_a: a, y_b: b} (DED x_a NEQ y_a ⟶ DED x_b NEQ y_b) ⟶ (DED x_b EQ y_b ⟶ DED x_a EQ y_a) ❘ # contra 3 4 5 6 7 ❙
	trans_equal: {a: type, w: a, x: a, y: a, z: a} DED w EQ x ⟶ DED z EQ y ⟶ DED x EQ y ⟶ DED w EQ z ❘ # trans_eq 2 3 4 5 6 7 8 ❙
	cns_functionhood: {a: type, hd_0: a, tl_0: lst a, hd_1, tl_1} DED (hd_0 EQ hd_1) ⟶ DED tl_0 EQ tl_1 ⟶ DED (cns a hd_0 tl_0) EQ (cns a hd_1 tl_1) ❘ # cns_funct 2 3 4 5 6 7 ❙

	
	//cons_inj_0: {a:type, hd_0:a, tl_0: lst a, hd_1:a, tl_1: lst a} DED (cns a hd_0 tl_0) EQ (cns a hd_1 tl_1) ⟶ DED hd_0 EQ hd_1 ❘ = [a, hd_0, tl_0, hd_1,tl_1] contra hd_0 (cns a hd_0 tl_0) hd_1 (cns a hd_1 tl_1) (list1/injective_cons_0 a hd_0 tl_0 hd_1 tl_1) ❙
	//cons_inj_1: {a:type, hd_0:a, tl_0: lst a, hd_1:a, tl_1: lst a} DED (cns a hd_0 tl_0) EQ (cns a hd_1 tl_1) ⟶ DED tl_0 EQ tl_1 ❘ = [a, hd_0, tl_0, hd_1,tl_1] contra tl_0 (cns a hd_0 tl_0) tl_1 (cns a hd_1 tl_1) (list1/injective_cons_1 a hd_0 tl_0 hd_1 tl_1) ❙
	//consArgs: {a: type} type ❘ = [a] a * (lst a) ❙
	//consP: {a: type} consArgs a ⟶ lst a ❘ = [a, args] cns a (pair/a a (lst a) args) (pair/b a (lst a) args) ❙
	// This should work:❙
	// test: {a: type, hd_0: a, tl_0: lst a, hd_1:a, tl_1: lst a} DED (cns a hd_0 tl_0) EQ (cns a hd_1 tl_1) ⟶ DED hd_0 EQ hd_1 ❘ = [a, hd_0, tl_0, hd_1, tl_1] (cons_inj_0 a hd_0 tl_0 hd_1 tl_1) ❙
	// inj_cons: {a: type, hd_0: a, tl_0: lst a, hd_1:a, tl_1: lst a} DED (cns a hd_0 tl_0) EQ (cns a hd_1 tl_1) ⟶ DED pair/make a (lst a) hd_0 tl_0 EQ pair/make a (lst a) hd_1 tl_1 ❘ 
	= [a, hd_0, tl_0, hd_1, tl_1, P] pair/equiv a (lst a) hd_0 tl_0 hd_1 tl_1 (cons_inj_0 a hd_0 tl_0 hd_1 tl_1 P) (cons_inj_1 a hd_0 tl_0 hd_1 tl_1 P) ❙

	// This is correct, but not accepted by the typechecker
	// For the typechecker to see this a (typelevel) definition expansion of consP is required ❙
	// inj_consP_weak: {a: type, args_0: consArgs a, args_1: consArgs a} DED (consP a args_0) EQ (consP a args_1) ⟶ 
		DED pair/make a (lst a) (pair/a a (lst a) args_0) (pair/b a (lst a) args_0) EQ pair/make a (lst a) (pair/a a (lst a) args_1) (pair/b a (lst a) args_1) 
	❘ = [a, args_0, args_1, P] (inj_cons a (pair/a a (lst a) args_0) (pair/b a (lst a) args_0) (pair/b a (lst a) args_1) (pair/b a (lst a) args_1)) P ❙
	// inj_consP: {a: type, args_0: consArgs a, args_1: consArgs a, P: DED (consP a args_0) EQ (consP a args_1)} DED args_0 EQ args_1 ❘ = [a, args_0, args_1, P] 
		trans_equal (a*(lst a)) args_0 (pair/make a (lst a) (pair/a a (lst a) args_0) (pair/b a (lst a) args_0)) (pair/make a (lst a) (pair/a a (lst a) args_1) (pair/b a (lst a) args_1)) args_1
	 (pair/repr a (lst a) (pair/a a (lst a) args_0) (pair/b a (lst a) args_0) args_0)
	 (pair/repr a (lst a) (pair/a a (lst a) args_1) (pair/b a (lst a) args_1) args_1)
	 (inj_consP_weak a args_0 args_1 P) ❙
	
	list: type ⟶ type ❘ = [a] list3/list a ❙
	//inj_cons_1: {a:type, hd_0:a, tl_0: list a, hd_1:a, tl_1: list a} DED hd_0 NEQ hd_1 ⟶ DED (hd_0 ∷ tl_0) NEQ (hd_1 ∷ tl_1) ❘ = [a, hd_0, tl_0, hd_1, tl_1] list3/injective_cons_0 a hd_0  tl_0 hd_1 tl_1 ❙
	//inj_cons_2: {a:type, hd_0:a, tl_0: list a, hd_1:a, tl_1: list a} DED tl_0 NEQ tl_1 ⟶ DED (hd_0 ∷ tl_0) NEQ (hd_1 ∷ tl_1) ❘ = [a, hd_0, tl_0, hd_1, tl_1] list3/injective_cons_1 a hd_0  tl_0 hd_1 tl_1 ❙
	//weak_inj_cons_1: {a:type, hd_0:a, hd_1:a, tl:list3/list a} DED hd_0 NEQ hd_1 ⟶ DED (hd_0 ∷ tl) NEQ (hd_1 ∷ tl) ❘ = [a, hd_0, hd_1, tl] list3/injective_cons_0 a hd_0 tl hd_1 tl ❙
	//weak_inj_cons_2: {a:type, hd:a, tl_0:list3/list a, tl_1:list3/list a} DED tl_0 NEQ tl_1 ⟶ DED (hd ∷ tl_0) NEQ (hd ∷ tl_1) ❘ = [a, hd, tl_0, tl_1] list3/injective_cons_1 a hd tl_0 hd tl_1 ❙
❚

// theory UniversalPropertyFreeMonoid : ?InductivelyDefinedTypes =
// 	inductive unitType() ❘ =
// 		tp: type ❙
// 		tm: unitType ❙
// 	❚
// 	unit: type ❘ = unitType/tp ❙
// 	plus_assoc: {x: nat/n, y: nat/n, z: nat/n} DED nat/plus/n (nat/plus/n x y) z EQ nat/plus/n x (nat/plus/n y z) ❙
// 	zero_plus: {x: nat/n} DED nat/plus/n nat/z x EQ nat/z ❙
// 	plus_zero: {x: nat/n} DED nat/z EQ nat/plus/n x nat/z ❙

// 	inductive_definition Nat(): freeMonoid(unit) ❘ =
// 		fm: type ❘ = nat/n ❙
// 		gen: a ⟶ fm ❘ = unitType/induct/tm nat/n (nat/s nat/z) ❙
// 		unit: fm ❘ = nat/z ❙
// 		comp: fm ⟶ fm ⟶ fm ❘ = [a, b] nat/plus/n a b ❙
// 		assoc: {x: fm, y: fm, z: fm} DED comp (comp x y) z EQ comp x (comp y z) ❘ = [x, y, z] plus_assoc x y z ❙
// 		unit_r: {x: fm} DED comp x unit EQ x ❘ = [x] zero_plus x ❙
// 		unit_l: {x: fm} DED comp unit x EQ x ❘ = [x] plus_zero x ❙
// 	❚
// ❚

/T The following definition of surreal numbers won't typecheck (as expected), but is a nice pathological example ❙
// theory SurrealNumbers : ?LFXI =
	linear_order: {A: type} A ⟶ type ❙
//	ordBddAboveSet: {A: type, ord: linear_order A} A ⟶ kind ❙
//	ordBddBelowSet: {A: type, ord: linear_order A} A ⟶ kind ❙
	
//	inductive surreal() ❘ =
//		sur: type ❙
//		ord: linear_order sur ❙
//		makeSurreal: {a: sur} (ordBddAboveSet sur ord a) (ordBddBelowSet sur ord a) sur ❙
//	
// ❚