(* Basic definitions for LEGO exercises *) Module basic; [Set = Type(0)]; [TYPE = Type]; (* True *) Inductive [True : Set] Constructors [triv : True]; (* Sigma types *) Inductive [Sigma : Set] Parameters [A?Set][B?A->Set] Constructors [pair : {a:A}{b:B a}Sigma]; [fst = Sigma_elim ([_:Sigma]A) ([a:A][b:B a]a)]; [snd = Sigma_elim ([p:Sigma]B (fst p)) ([a:A][b:B a]b)]; Discharge A; (* False *) Inductive [False : Set]; (* Disjoint union *) Inductive [Plus : Set] Parameters [A,B?Set] Constructors [inl : A -> Plus] [inr : B -> Plus]; [case[C|Set] = Plus_elim ([_:Plus]C)]; Discharge A; (* Derived connectives *) [And[A,B:Set] = Sigma [_:A]B]; [pair'[A,B|Set][a:A][b:B] = pair|A|([_:A]B) a b]; [iff[A,B:Set] = And (A -> B) (B -> A)]; [not[A:Set] = A -> False]; (* Equality *) Inductive [Id : A->A->Set] Parameters [A?Set] Constructors [refl : {a:A}Id a a]; [C:A->Set]; Goal {a,b|A}(Id a b)->(C a)->(C b); Intros; Refine Id_elim ([x,y:A][_:Id x y](C x)->(C y)); Intros; Immed; Immed; Save subst; Discharge C; Goal {a,b|A}(Id a b)->(Id b a); Intros; Refine subst ([x:A]Id x a); Next +1; Refine H; Refine refl; Save sym; Goal {a,b,c|A}(Id a b)->(Id b c)->(Id a c); Intros; Refine subst; Next +1; Refine H1; Refine H; Save trans; Discharge A; [A,B|Set]; Goal {f:A->B}{a,b|A}(Id a b)->(Id (f a) (f b)); Intros; Refine subst [x:A]Id (f a) (f x); Next +1; Refine H; Refine refl; Save resp; Discharge A; (* Natural numbers *) Inductive [Nat:Set] Constructors [ze : Nat] [su : Nat -> Nat]; [n1 = su ze]; [n2 = su n1]; [ind = Nat_elim]; [prec[A|Type] = Nat_elim [n:Nat]A]; [add = prec ([n:Nat]n) ([m:Nat][add_m:Nat->Nat][n:Nat]su (add_m n))]; [consN = [n:Nat][p:Id ze (su n)] subst (prec True ([_:Nat][_:Set]False)) p triv : {n:Nat}not (Id ze (su n))]; (* Goal {n:Nat}not (Id ze (su n)); Intros; Refine prec True ([_:Nat][_:Set]False) (su n); Error: doesn't solve goal why??? *)