-- File: LOLP_Axioms -- This file introduces axioms for records and existential types. Path "../lol" Path "../lolExtra" Load "lambdaLplus" Load "logic2" ------------- -- records -- ------------- -- We introduce the induction axiom for records only for two-field record with -- labels 'l' and 'r' (See Remark 6.2.2.) Var ind_rec : @A,B:*s. @P:{|l:A,r:B|} ->*p. (@a:A.@b:B. P {l=a,r=b}) -> @z:{|l:A,r:B|}. P z -- exhaustion property follows from axiom Prove exh_rec : @A,B:*s. @z:{|l:A,r:B|}. Ex a:A.Ex b:B. z={l=a,r=b} Intros 2 Apply ind_rec Intros ExistsI a ExistsI b Refl Exit -- an additional property Prove is_rec : @A,B:*s. @x,y:{|l:A,r:B|}. x`l=y`l -> x`r = y`r -> x=y Intros 2 Apply ind_rec Intros 2 Apply ind_rec Intros Rewrite H Rewrite H1 Refl Exit ----------------------- -- existential types -- ----------------------- -- We introduce the induction axiom for existential types only for kind *s.(See -- Remark 6.2.2.) Var ind_sigma : @I:*s->*s. @P:(Sig X:*s.I X) -> *p. (@A:*s.@a:I A. P (pack I A a)) -> @z:(Sig X:*s. I X). P z -- exhaustion property follows from axiom Prove exh_sigma : @I:*s->*s. @z:(Sig X:*s. I X). ExK A:*s. Ex a:I A. z = pack I A a Intro Apply ind_sigma Intros ExistsI A ExistsI a Refl Exit