include "topology/igft.ma".
-nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
-nnormalize; nauto;
-nqed.
+nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V./2/.nqed.
ninductive Sigma (A: Type[0]) (P: A → CProp[0]) : Type[0] ≝
mk_Sigma: ∀a:A. P a → Sigma A P.
#A; #U; #a; #H; nelim H
[ #n; #H1; @1; nassumption
| #a; #i; #IH; #H; @2 [ napply i ] #y; *; #j; #E; nrewrite > E; ncases j; #x; #K;
- napply H; nnormalize; nassumption.
+ napply H; nnormalize; //.
nqed.
ndefinition ncoverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
(U ⊆ P) → (∀a:A.∀i:𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j. 𝐝 a i j ∈ P) → a ∈ P) →
◃ U ⊆ P.
#A; #U; #P; #refl; #infty; #a; #H; nelim H
- [ nauto | (*nauto depth=4;*) #b; #j; #K1; #K2;
- napply infty; nauto; ##]
+ [ // | #b; #j; #K1; #K2; napply infty; //; ##]
nqed.
alias symbol "covers" (instance 3) = "ncovers".
nlemma eq_rect_Type0_r':
∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
- #A; #a; #x; #p; ncases p; nauto;
+ #A; #a; #x; #p; ncases p; //;
nqed.
nlemma eq_rect_Type0_r:
∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); //.
nqed.
nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
≝ ?.
nlapply (decide_mem_ok … memdec b); nlapply (decide_mem_ko … memdec b);
ncases (decide_mem … memdec b)
- [ #_; #H; napply refl; nauto
- | #H; #_; ncut (uuC … b=uuC … b) [nauto] ncases (uuC … b) in ⊢ (???% → ?)
- [ #E; napply False_rect_Type0; ncut (b=b) [nauto] ncases p in ⊢ (???% → ?)
- [ #a; #K; #E2; napply H [ nauto | nrewrite > E2; nauto ]
+ [ #_; #H; napply refl; /2/
+ | #H; #_; ncut (uuC … b=uuC … b) [//] ncases (uuC … b) in ⊢ (???% → ?)
+ [ #E; napply False_rect_Type0; ncut (b=b); //; ncases p in ⊢ (???% → ?)
+ [ #a; #K; #E2; napply H; //; nrewrite > E2; //
##| #a; #i; #K; #E2; nrewrite < E2 in i; nnormalize; nrewrite > E; nnormalize;
- nauto]
+ //]
##| #a; #E;
ncut (a ◃ U)
- [ nlapply E; nlapply (H ?) [nauto] ncases p
+ [ nlapply E; nlapply (H ?) [//] ncases p
[ #x; #Hx; #K1; #_; ncases (K1 Hx)
##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
nrewrite > E2; nnormalize; /2/ ]##]
nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
napply (H2 one); #y
[ napply Hcut
- ##| napply (cover_rect A U memdec P refl infty a); nauto ]
+ ##| napply (cover_rect A U memdec P refl infty a); // ]
##| #a; #a1; #E;
ncut (a ◃ U)
- [ nlapply E; nlapply (H ?) [nauto] ncases p
+ [ nlapply E; nlapply (H ?) [//] ncases p
[ #x; #Hx; #K1; #_; ncases (K1 Hx)
##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
nrewrite > E2; nnormalize; #_; @1 (true); /2/ ]##]
#Hcut;
ncut (a1 ◃ U)
- [ nlapply E; nlapply (H ?) [nauto] ncases p
+ [ nlapply E; nlapply (H ?) [//] ncases p
[ #x; #Hx; #K1; #_; ncases (K1 Hx)
##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
nrewrite > E2; nnormalize; #_; @1 (false); /2/ ]##]
nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
napply (H2 one); #y; ncases y; nnormalize
[##1,2: nassumption
- | napply (cover_rect A U memdec P refl infty a); nauto
- | napply (cover_rect A U memdec P refl infty a1); nauto]
+ | napply (cover_rect A U memdec P refl infty a); //
+ | napply (cover_rect A U memdec P refl infty a1); //]
nqed.
(********* Esempio:
ntheorem skipfact_partial:
∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O).
- #n; nelim n
- [ @1; nnormalize; @1
- | #m; nelim m; nnormalize
- [ #H; @2; nnormalize
- [ //
- | #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; // ]
- ##| #p; #H1; #H2; @2; nnormalize
- [ //
- | #y; *; #a; #E; nrewrite > E; ncases a; nnormalize;
- nrewrite < (plus_n_Sm …); // ]##]
+ #n; nelim n; /2/;
+ #m; nelim m; nnormalize
+ [ #H; @2; nnormalize; //;
+ #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; //
+ ##| #p; #H1; #H2; @2; nnormalize; //;
+ #y; *; #a; #E; nrewrite > E; ncases a; nnormalize;
+ nrewrite < (plus_n_Sm …); // ]
nqed.
ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.
napply (S m * H true * H false) ]
nqed.
-nlemma test: skipfact four ? = four * two * two. ##[##2: napply (skipfact_partial two)]
- nnormalize; //.
+nlemma test: skipfact four ? = four * two * two. ##[##2: napply (skipfact_partial two)]//.
nqed.
\ No newline at end of file