nqed.
nlemma eq_ind_r_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.b = a → P b.
-#A; #a; #P; #p; #b; #E; ncases E in p; nauto;
+#A; #a; #P; #p; #b; #E; ncases E in p; //;
nqed.
nlemma csc :
//; nqed.
ntheorem transitive_eq : ∀A:Type. transitive A (eq A).
-//; nqed.
+#A; #x; #y; #z; #H1; #H2; nrewrite > H1; //; nqed.
ntheorem symmetric_not_eq: ∀A:Type. symmetric A (λx,y.x ≠ y).
-/2/; nqed.
+#A; #x; #y; #H; #K; napply H; napply symmetric_eq; //; nqed.
ntheorem eq_f: ∀A,B:Type.∀f:A→B.∀x,y:A. x=y → f x = f y.
-//; nqed.
+#A; #B; #f; #x; #y; #H; nrewrite > H; //; nqed.
(*
theorem eq_f': \forall A,B:Type.\forall f:A\to B.
ntheorem eq_f2: ∀A,B,C:Type.∀f:A→B→C.
∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
-//; nqed.
\ No newline at end of file
+#A; #B; #C; #f; #x1; #x2; #y1; #y2; #E1; #E2; nrewrite > E1; nrewrite > E2;//.
+nqed.
\ No newline at end of file
-algebra/bool.ma logic/connectives.ma
overlap/o-algebra.ma sets/categories2.ma
+algebra/bool.ma logic/connectives.ma
algebra/abelian_magmas.ma algebra/magmas.ma
-logic/destruct_bb.ma logic/equality.ma
+basics/functions.ma Plogic/connectives.ma Plogic/equality.ma
+Plogic/connectives.ma Plogic/equality.ma
+arithmetics/nat.ma basics/eq.ma basics/functions.ma
datatypes/bool.ma logic/pts.ma
+logic/destruct_bb.ma logic/equality.ma
logic/equality.ma logic/connectives.ma properties/relations.ma
sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma
logic/cprop.ma hints_declaration.ma sets/setoids1.ma
topology/igft.ma logic/equality.ma sets/sets.ma
-algebra/magmas.ma sets/sets.ma
nat/minus.ma nat/order.ma
+algebra/magmas.ma sets/sets.ma
hints_declaration.ma logic/pts.ma
Plogic/equality.ma logic/pts.ma
properties/relations1.ma logic/pts.ma
-sets/categories.ma sets/sets.ma
algebra/unital_magmas.ma algebra/magmas.ma
nat/compare.ma datatypes/bool.ma nat/order.ma
+sets/categories.ma sets/sets.ma
properties/relations2.ma logic/pts.ma
nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma
logic/connectives.ma logic/pts.ma
+basics/relations.ma Plogic/connectives.ma
topology/igft-setoid.ma sets/sets.ma
sets/categories2.ma sets/categories.ma sets/setoids2.ma sets/sets.ma
sets/sets.ma hints_declaration.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
-logic/pts.ma
-nat/order.ma nat/nat.ma sets/sets.ma
-nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma
datatypes/pairs.ma logic/pts.ma
-sets/setoids1.ma hints_declaration.ma properties/relations1.ma sets/setoids.ma
+nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma
+nat/order.ma nat/nat.ma sets/sets.ma
+logic/pts.ma
topology/cantor.ma nat/nat.ma topology/igft.ma
-sets/setoids2.ma properties/relations2.ma sets/setoids1.ma
+sets/setoids1.ma hints_declaration.ma properties/relations1.ma sets/setoids.ma
nat/big_ops.ma algebra/magmas.ma nat/order.ma
-topology/igft2.ma topology/igft.ma
+sets/setoids2.ma properties/relations2.ma sets/setoids1.ma
+topology/igft2.ma arithmetics/nat.ma topology/igft.ma
+topology/igft3.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma
properties/relations.ma logic/pts.ma
-sets/setoids.ma logic/connectives.ma properties/relations.ma
+basics/eq.ma basics/relations.ma
+sets/setoids.ma hints_declaration.ma logic/connectives.ma properties/relations.ma
include "logic/equality.ma".
+ninductive unit: Type[0] ≝ k: unit.
+
+ninductive bool: unit → Type[0] ≝ true : bool k | false : bool k.
+
+nlemma foo: true = false → False. #H; ndestruct;
+
(* nlemma prova : ∀T:Type[0].∀a,b:T.∀e:a = b.
∀P:∀x,y:T.x=y→Prop.P a a (refl T a) → P a b e.
#T;#a;#b;#e;#P;#H;
#s; #s1; @ (unary_morphism1 s s1); @
[ #f; #g; napply (∀a:s. f a = g a)
| #x; #a; napply refl1
- | #x; #y; #H; #a; napply sym1; nauto
+ | #x; #y; #H; #a; napply sym1; //
| #x; #y; #z; #H1; #H2; #a; napply trans1; ##[##2: napply H1 | ##skip | napply H2]##]
nqed.
nqed.
nlemma hint_auto1 : ∀A,U,V. (∀x.x ∈ U → x ◃ V) → cover_set cover A U V.
-nnormalize; nauto.
+nnormalize; /2/.
nqed.
alias symbol "covers" (instance 1) = "covers".
alias symbol "covers" (instance 2) = "covers set".
alias symbol "covers" (instance 3) = "covers".
ntheorem transitivity: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
-#A; #a; #U; #V; #aU; #UV; nelim aU; nauto depth=4;
+#A; #a; #U; #V; #aU; #UV; nelim aU; /3/;
nqed.
ndefinition emptyset: ∀A.Ω^A ≝ λA.{x | False}.
∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i.
#A; #a; #H; nelim H;
##[ #n; *;
-##| #b; #i_star; #IH1; #IH2; ncases (EM … b i_star); nauto;
+##| #b; #i_star; #IH1; #IH2; ncases (EM … b i_star); /2/;
##]
nqed.
ndefinition uax : uAx → Ax.
#A; @ (uax_ A) (λx.unit); #a; #_;
-napply (𝐂 a ?); nlapply one; ncases (with_ A a); nauto;
+napply (𝐂 a ?); nlapply one; ncases (with_ A a); //;
nqed.
ncoercion uax : ∀u:uAx. Ax ≝ uax on _u : uAx to Ax.
∀A:uAx.∀a:A. a ◃ ∅ → ¬ a ∈ 𝐂 a one.
#A; #a; #H; nelim H;
##[ #n; *;
-##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 … H3); nauto;
+##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 … H3); //;
##]
nqed.
ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }.
ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V.
-#A; #a; #U; #V; #HUV; #H; nelim H; nauto depth=4;
+#A; #a; #U; #V; #HUV; #H; nelim H; //;
nqed.
ntheorem th3_1: ¬∃a:axs.Z ⊆ S a ∧ S a ⊆ Z.
ncut (a ◃ Z); ##[
nlapply (axiom_cond … a one); #AxCon; nchange in AxCon with (a ◃ S a);
napply (cover_monotone … AxCon); nassumption; ##] #H;
-ncut (a ◃ ∅); ##[ napply (transitivity … H); nwhd in match Z; nauto; ##] #H1;
+ncut (a ◃ ∅); ##[ napply (transitivity … H); nwhd in match Z; //; ##] #H1;
ncut (¬ a ∈ S a); ##[ napply (col2_4 … H1); ##] #H2;
ncut (a ∈ S a); ##[ napply ZSa; napply H1; ##] #H3;
-nauto;
+//;
nqed.
include "nat/nat.ma".
nlemma replace_char:
∀A:Ax.∀U,V.U ⊆ V → V ⊆ U → ∀a:A.a ◃ U → a ◃ V.
-#A; #U; #V; #UV; #VU; #a; #aU; nelim aU; nauto;
+#A; #U; #V; #UV; #VU; #a; #aU; nelim aU; //;
nqed.
ntheorem th_ch3: ¬∃a:caxs.∀x.ϕ a x = h x.
*; #a; #H;
ncut (a ◃ { x | x ◃ ∅}); ##[
- napply (replace_char … { x | h x = O }); ##[ ##1,2: #x; ncases (Ph x); nauto; ##]
- napply (replace_char … { x | ϕ a x = O }); ##[##1,2: #x; nrewrite > (H x); nauto; ##]
+ napply (replace_char … { x | h x = O }); ##[ ##1,2: #x; ncases (Ph x); //; ##]
+ napply (replace_char … { x | ϕ a x = O }); ##[##1,2: #x; nrewrite > (H x); //; ##]
napply (axiom_cond … a one); ##] #H1;
-ncut (a ◃ ∅); ##[ napply (transitivity … H1); nauto; ##] #H2;
+ncut (a ◃ ∅); ##[ napply (transitivity … H1); //; ##] #H2;
nlapply (col2_4 …H2); #H3;
ncut (a ∈ 𝐂 a one); ##[
- nnormalize; ncases (Ph a); nrewrite > (H a); nauto; ##] #H4;
-nauto;
+ nnormalize; ncases (Ph a); nrewrite > (H a); //; ##] #H4;
+//;
nqed.
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:
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
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.
(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:
≝ ?.
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:
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
projects / helm.git / commitdiff