alias symbol "eq" = "setoid eq".
alias symbol "eq" = "setoid1 eq".
alias symbol "eq" = "setoid eq".
+alias symbol "eq" = "setoid1 eq".
nrecord partition (A: setoid) : Type[1] ≝
{ support: setoid;
indexes: qpowerclass support;
nlapply
(iso_nat_nat_union_uniq n s nindex (fst … (iso_nat_nat_union s xxx n))
nindex2 (snd … (iso_nat_nat_union s xxx n)) ?????)
- [##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl
- | napply le_S_S_to_le; nassumption
+ [##6: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl
+ |##5: napply le_S_S_to_le; nassumption
|##*: nassumption]##]
##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;
- ngeneralize in match (? : ∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ pc ? (Nat_ (s i1)) → i2' ∈ pc ? (Nat_ (s i1')) → eq_rel (carr A) (eq A) (iso_f ???? (fi i1) i2) (iso_f ???? (fi i1') i2') → i1=i1' ∧ i2=i2') in ⊢ ?
- [##2: #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
- ngeneralize in match (disjoint ? P (iso_f ???? f i1) (iso_f ???? f i1') ???) in ⊢ ?
+ ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ pc ? (Nat_ (s i1)) → i2' ∈ pc ? (Nat_ (s i1')) → eq_rel (carr A) (eq A) (iso_f ???? (fi i1) i2) (iso_f ???? (fi i1') i2') → i1=i1' ∧ i2=i2');
+ ##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
+ nlapply(disjoint … P (f i1) (f i1') ???)
[##2,3: napply f_closed; nassumption
- |##4: napply ex_intro [ napply (iso_f ???? (fi i1) i2) ] napply conj
- [ napply f_closed; nassumption ##| napply (. ?‡#) [ nassumption | ##2: ##skip]
- nwhd; napply f_closed; nassumption]##]
- #E'; ngeneralize in match (? : i1=i1') in ⊢ ?
- [##2: napply (f_inj … E'); nassumption
- | #E''; nrewrite < E''; napply conj
- [ napply refl | nrewrite < E'' in E; #E'''; napply (f_inj … E''')
+ |##1: @ (fi i1 i2); @;
+ ##[ napply f_closed; nassumption ##| napply (. E‡#);
+ nwhd; napply f_closed; nassumption]##]
+ #E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); nassumption; ##]
+ #E''; nrewrite < E''; @;
+ ##[ @;
+ ##| nrewrite < E'' in E; #E'''; napply (f_inj … E''')
[ nassumption | nrewrite > E''; nassumption ]##]##]
##] #K;
nelim (iso_nat_nat_union_char n s x Hx); *; #i1x; #i2x; #i3x;
nelim (iso_nat_nat_union_char n s x' Hx'); *; #i1x'; #i2x'; #i3x';
- ngeneralize in match (K … E) in ⊢ ?
- [##2,3: napply le_to_le_S_S; nassumption
- |##4,5: nassumption]
+ nlapply (K … E)
+ [##1,2: nassumption;
+ ##|##3,4:napply le_to_le_S_S; nassumption; ##]
*; #K1; #K2;
napply (eq_rect_CProp0_r ?? (λX.λ_.? = X) ?? i1x');
napply (eq_rect_CProp0_r ?? (λX.λ_.X = ?) ?? i1x);
[ napply (qpowerclass A)
| napply (qseteq A) ]
nqed.
-
+
unification hint 0 ≔ A ⊢
- carr1 (qpowerclass_setoid A) ≡ qpowerclass A.
+ carr1 (mk_setoid1 (qpowerclass A) (eq1 (qpowerclass_setoid A)))
+≡ qpowerclass A.
-(*CSC: non va!
-unification hint 0 ≔ A ⊢
- carr1 (mk_setoid1 (qpowerclass A) (eq1 (qpowerclass_setoid A))) ≡ qpowerclass A.*)
+ncoercion pc' : ∀A.∀x:qpowerclass_setoid A. Ω^A ≝ pc
+on _x : (carr1 (qpowerclass_setoid ?)) to (Ω^?).
nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP.
#A; @
##]
nqed.
-(*CSC: bug qui se metto x o S al posto di ?
-nlemma foo: True.
-nletin xxx ≝ (λA:setoid.λx,S. let SS ≝ pc ? S in
- fun21 ??? (mk_binary_morphism1 ??? (λx.λS. ? ∈ ?) (prop21 ??? (mem_ok A))) x S);
-*)
unification hint 0 ≔ A:setoid, x, S;
- SS ≟ (pc ? S)
+ SS ≟ (pc ? S),
+ TT ≟ (mk_binary_morphism1 ???
+ (λx:setoid1_of_setoid ?.λS:qpowerclass_setoid ?. x ∈ S)
+ (prop21 ??? (mem_ok A)))
+
(*-------------------------------------*) ⊢
- fun21 ??? (mk_binary_morphism1 ??? (λx,S. x ∈ S) (prop21 ??? (mem_ok A))) x S ≡ mem A SS x.
+ fun21 ? ? ? TT x S
+ ≡ mem A SS x.
nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP.
#A; @
(*-----------------------------------------------------------------*) ⊢
eq_rel ? (eq A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'.
+nlemma intersect_ok: ∀A. qpowerclass A → qpowerclass A → qpowerclass A.
+ #A; #S; #S'; @ (S ∩ S');
+ #a; #a'; #Ha; @; *; #H1; #H2; @
+ [##1,2: napply (. Ha^-1‡#); nassumption;
+##|##3,4: napply (. Ha‡#); nassumption]
+nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 1 ≔
+ A : setoid, B,C : qpowerclass A ⊢
+ pc A (mk_qpowerclass ? (B ∩ C) (mem_ok' ? (intersect_ok ? B C)))
+ ≡ intersect ? (pc ? B) (pc ? C).
+
+nlemma intersect_ok': ∀A. binary_morphism1 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A).
+ #A; @ (λS,S'. S ∩ S');
+ #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *; #Ka; #Kb; @
+ [ napply Ha1; nassumption
+ | napply Hb1; nassumption
+ | napply Ha2; nassumption
+ | napply Hb2; nassumption]
+nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔
+ A : Type[0], B,C : powerclass A ⊢
+ fun21 …
+ (mk_binary_morphism1 …
+ (λS,S'.S ∩ S')
+ (prop21 … (intersect_ok' A))) B C
+ ≡ intersect ? B C.
+
+ndefinition prop21_mem :
+ ∀A,C.∀f:binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) C.
+ ∀a,a':setoid1_of_setoid A.
+ ∀b,b':qpowerclass_setoid A.a = a' → b = b' → f a b = f a' b'.
+#A; #C; #f; #a; #a'; #b; #b'; #H1; #H2; napply prop21; nassumption;
+nqed.
+
+interpretation "prop21 mem" 'prop2 l r = (prop21_mem ??????? l r).
+
+
+nlemma test: ∀U.∀A,B:qpowerclass U. A ∩ B = A →
+ ∀x,y. x=y → x ∈ A → y ∈ A ∩ B.
+ #U; #A; #B; #H; #x; #y; #K; #K2; napply (. K^-1‡H); nassumption;
+nqed.
+
+(*
nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A).
#A; @
[ #S; #S'; @
alias symbol "hint_decl" = "hint_decl_Type1".
unification hint 0 ≔
A : setoid, B,C : qpowerclass A ⊢
- pc A (intersect_ok A B C) ≡ intersect ? (pc ? B) (pc ? C).
+ pc A (fun21 …
+ (mk_binary_morphism1 …
+ (λS,S':qpowerclass_setoid A.mk_qpowerclass ? (S ∩ S') (mem_ok' ? (intersect_ok ? S S')))
+ (prop21 … (intersect_ok A)))
+ B
+ C)
+ ≡ intersect ? (pc ? B) (pc ? C).
nlemma test: ∀A:setoid. ∀U,V:qpowerclass A. ∀x,x':setoid1_of_setoid A. x=x' → x ∈ U ∩ V → x' ∈ U ∩ V.
#A; #U; #V; #x; #x'; #H; #p; napply (. (H^-1‡#)); nassumption.
nqed.
+*)
ndefinition image: ∀A,B. (carr A → carr B) → Ω^A → Ω^B ≝
λA,B:setoid.λf:carr A → carr B.λSa:Ω^A.
-----------------------------------------------------
In this appendix we try to give a description of tactics
-in terms of natural deduction rules annotated with proofs.
+in terms of sequent calculus rules annotated with proofs.
The `:` separator has to be read as _is a proof of_, in the spirit
of the Curry-Howard isomorphism.
- f : A1 → … → An → B ?1 : A1 … ?n : An
- napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
- (f ?1 … ?n ) : B
+ Γ ⊢ f : A1 → … → An → B Γ ⊢ ?1 : A1 … ?n : An
+ napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ ⊢ (f ?1 … ?n ) : B
foo
- [x : T]
- ⋮
- ? : P(x)
+ Γ; x : T ⊢ ? : P(x)
#x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
- λx:T.? : ∀x:T.P(x)
+ Γ ⊢ λx:T.? : ∀x:T.P(x)
baz
- (?1 args1) : P(k1 args1) … (?n argsn) : P(kn argsn)
- ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
- match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n : P(x)
+ Γ; args… : Args… ⊢ ?i : P(k1 args1) … (?n argsn) : P(kn argsn)
+ ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ ⊢ match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n : P(x)
bar
projects / helm.git / commitdiff