include "topology/igft.ma".
nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
-nnormalize; nauto;
+nnormalize; /2/;
nqed.
alias symbol "covers" = "covers set".
∀A:Ax.∀U,P:Ω^A.
(U ⊆ P) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → 𝐂 a 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; ##]
+ #A; #U; #P; #refl; #infty; #a; #H; nelim H; /3/.
nqed.
alias symbol "covers" (instance 1) = "covers".
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:
≝ ?.
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; #_; nauto]##]
+ nrewrite > E2; nnormalize; #_; //]##]
#Hcut;
nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
napply (H2 one); #y; #E2; nrewrite > E2
- (* [##2: napply cover_rect] nauto depth=1; *)
+ (* [##2: napply cover_rect] //; *)
[ napply Hcut
- ##| napply (cover_rect A U memdec P refl infty a); nauto ]##]
+ ##| napply (cover_rect A U memdec P refl infty a); // ]##]
nqed.
(********* Esempio:
| S m ⇒ S m * skipfact (pred m) ]
**)
-ntheorem psym_plus: ∀n,m. n + m = m + n.
- #n; nelim n
- [ #m; nelim m; //; #n0; #H;
- nchange with (natS n0 = natS (n0 + O));
- nrewrite < H; //
- | #n0; #H; #m; nchange with (S (n0 + m) = m + S n0);
- nrewrite > (H …);
- nelim m; //;
- #n1; #E; nrewrite > E; //]
+ntheorem psym_plus: ∀n,m. n + m = m + n.//.
nqed.
-nlemma easy1: ∀n:nat. two * (S n) = two + two * n.
- #n; nelim n;//;
- #n0; #H; nnormalize;
- nrewrite > (psym_plus ??);
- nrewrite > H; nnormalize;
- nrewrite > (psym_plus ??);
- //.
+nlemma easy1: ∀n:nat. two * (S n) = two + two * n.//.
nqed.
ndefinition skipfact_dom: uuAx.
| #m; #H; @2
[ nnormalize; @1
| nnormalize; #y; nchange in ⊢ (% → ?) with (y = pred (pred (two * (natone + m))));
- nrewrite > (easy1 …); nchange in ⊢ (% → ?) with (y = two * m);
- #E; nrewrite > E; nassumption ]##]
+ nnormalize; nrewrite < (plus_n_Sm …); nnormalize;
+ #E; nrewrite > E; napply H ]##]
nqed.
ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.
napply (S m * H (pred m) …); //]
nqed.
-nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)]
- nnormalize; //.
+nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)] //.
nqed.
\ No newline at end of file