(* NOTE: OEIS sequence identifiers
P(n): A016777 "3n+1"
-*)
+ T(n): A155504 "(3h+1)*3^(k+1)"
+*)
-inductive P: nat \to Prop \def
+inductive P: nat → Prop ≝
| p1: P 1
- | p2: \forall i,j. T i \to P j \to P (i + j)
-with T: nat \to Prop \def
- | t1: \forall i. P i \to T (i * 3)
- | t2: \forall i. T i \to T (i * 3)
+ | p2: ∀i,j. T i → P j → P (i + j)
+with T: nat → Prop ≝
+ | t1: ∀i. P i → T (i * 3)
+ | t2: ∀i. T i → T (i * 3)
.
-inductive S: nat \to Prop \def
- | s1: \forall i. P i \to S (i * 2)
- | s2: \forall i. T i \to S (i * 2)
+inductive S: nat → Prop ≝
+ | s1: ∀i. P i → S (i * 2)
+ | s2: ∀i. T i → S (i * 2)
.
include "classes/defs.ma".
-theorem p_inv_O: P 0 \to False.
+theorem p_inv_O: P 0 → False.
intros; inversion H; clear H; intros;
[ destruct
| lapply linear plus_inv_O3 to H3; decompose; destruct;
].
qed.
-theorem t_inv_O: T 0 \to False.
+theorem t_inv_O: T 0 → False.
intros; inversion H; clear H; intros;
[ lapply linear times_inv_O3_S to H1; destruct; autobatch depth = 2
| lapply linear times_inv_O3_S to H2; destruct; autobatch depth = 2
].
qed.
-theorem p_pos: \forall i. P i \to \exists k. i = S k.
+theorem p_pos: ∀i. P i → ∃k. i = S k.
intros 1; elim i names 0; clear i; intros;
[ lapply linear p_inv_O to H; decompose
| autobatch depth = 2
].
qed.
-theorem t_pos: \forall i. T i \to \exists k. i = S k.
+theorem t_pos: ∀i. T i → ∃k. i = S k.
intros 1; elim i names 0; clear i; intros;
[ lapply linear t_inv_O to H; decompose
| autobatch depth = 2
].
qed.
-theorem t_1: T 1 \to False.
+theorem t_1: T 1 → False.
intros; inversion H; clear H; intros;
[ lapply not_3_divides_1 to H1; decompose
| lapply not_3_divides_1 to H2; decompose
qed.
theorem t_3: T 3.
- change in \vdash (? %) with (1 * 3);
+ change in ⊢ (? %) with (1 * 3);
autobatch depth = 2.
qed.
-theorem pt_inv_gen: \forall i.
- (P i \to \exists h. i = S (h * 3)) \land
- (T i \to \exists h,k. i = S (h * 3) * 3 \sup (S k)).
+theorem pt_inv_gen: ∀i.
+ (P i → ∃h. i = S (h * 3)) ∧
+ (T i → ∃h,k. i = S (h * 3) * 3 \sup (S k)).
intros 1; elim i using wf_nat_ind names 0; clear i; intros; split; intros;
[ lapply linear p_inv_O to H; decompose
| lapply linear t_inv_O to H; decompose
| inversion H1; clear H1; intros;
- [ destruct; autobatch depth = 3 width = 50 size = 50
+ [ destruct; autobatch paramodulation
| clear H3; lapply t_pos to H1; lapply p_pos to H2; decompose; destruct;
lapply linear plus_inv_S_S_S to H4; decompose;
lapply H to H4; lapply H to H3; clear H H4 H3; decompose; clear H3 H4;
| clear H2; lapply linear times_inv_S_m_SS to H3 as H0;
lapply linear H to H0; decompose; clear H;
lapply linear H2 to H1; decompose; destruct;
- autobatch depth = 3
+ autobatch depth = 4
]
].
qed.
-theorem p_inv_gen: \forall i. P i \to \exists h. i = S (h * 3).
+theorem p_inv_gen: ∀i. P i → ∃h. i = S (h * 3).
intros; lapply depth = 1 pt_inv_gen; decompose;
lapply linear H1 to H as H0; autobatch depth = 1.
qed.
-theorem t_inv_gen: \forall i. T i \to \exists h,k. i = (S (h * 3)) * 3 \sup (S k).
+theorem t_inv_gen: ∀i. T i → ∃h,k. i = (S (h * 3)) * 3 \sup (S k).
intros; lapply depth = 1 pt_inv_gen; decompose;
lapply linear H2 to H as H0; autobatch depth = 2.
qed.
-theorem p_gen: \forall i. P (S (i * 3)).
+theorem p_gen: ∀i. P (S (i * 3)).
intros; elim i names 0; clear i; intros;
[ simplify; autobatch depth = 2
| rewrite > plus_3_S3n ; autobatch depth = 2
].
qed.
-theorem t_gen: \forall i,j. T (S (i * 3) * 3 \sup (S j)).
+theorem t_gen: ∀i,j. T (S (i * 3) * 3 \sup (S j)).
intros; elim j names 0; clear j; intros;
- [ simplify in \vdash (? (? ? %)); autobatch depth = 2
+ [ simplify in ⊢ (? (? ? %)); autobatch depth = 2
| rewrite > times_exp_x_y_Sz; autobatch depth = 2
].
qed.
alias num (instance 0) = "natural number".
-theorem plus_inv_O3: \forall m,n. 0 = n + m \to 0 = n \land 0 = m.
+theorem plus_inv_O3: ∀m,n. 0 = n + m → 0 = n ∧ 0 = m.
intros 2; elim n names 0; clear n; simplify; intros;
[ autobatch | destruct ].
qed.
-theorem times_inv_O3_S: \forall x,y. 0 = x * (S y) -> x = 0.
- intros; rewrite < times_n_Sm in H;
+theorem times_inv_O3_S: ∀x,y. 0 = x * (S y) → x = 0.
+ intros; rewrite < times_n_Sm in H;
lapply linear plus_inv_O3 to H; decompose; destruct; autobatch.
qed.
-theorem not_3_divides_1: \forall n. 1 = n * 3 \to False.
+theorem not_3_divides_1: ∀n. 1 = n * 3 → False.
intros 1; rewrite > sym_times; simplify;
elim n names 0; simplify; intros; destruct;
rewrite > sym_plus in Hcut; simplify in Hcut; destruct Hcut.
qed.
-theorem le_inv_S_S: \forall m,n. S m <= S n \to m <= n.
+theorem le_inv_S_S: ∀m,n. S m ≤ S n → m ≤ n.
intros; inversion H; clear H; intros; destruct; autobatch.
qed.
-theorem plus_inv_S_S_S: \forall x,y,z. S x = S y + S z \to S y <= x \land S z <= x.
+theorem plus_inv_S_S_S: ∀x,y,z. S x = S y + S z → S y ≤ x ∧ S z ≤ x.
simplify; intros; destruct;
- rewrite < plus_n_Sm in \vdash (? (? ? %) ?); autobatch depth = 3.
+ rewrite < plus_n_Sm in ⊢ (? (? ? %) ?); autobatch.
qed.
-theorem times_inv_S_m_SS: \forall k,n,m. S n = m * (S (S k)) \to m \le n.
+theorem times_inv_S_m_SS: ∀k,n,m. S n = m * (S (S k)) → m ≤ n.
intros 3; elim m names 0; clear m; simplify; intros; destruct;
clear H; apply le_S_S; rewrite < sym_times; simplify;
autobatch depth = 2.
qed.
-theorem plus_3_S3n: \forall n. S (S n * 3) = 3 + S (n * 3).
- intros; simplify; autobatch.
+theorem plus_3_S3n: ∀n. S (S n * 3) = 3 + S (n * 3).
+ intros; simplify; autobatch depth = 1.
qed.
-theorem times_exp_x_y_Sz: \forall x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
+theorem times_exp_x_y_Sz: ∀x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
intros; simplify; autobatch depth = 1.
qed.
-definition acc_nat \def \lambda P:nat \to Prop. \lambda n.
- \forall m. m <= n \to P m.
+definition acc_nat: (nat → Prop) → nat →Prop ≝
+ λP:nat→Prop. λn. ∀m. m ≤ n → P m.
-theorem wf_le: \forall P.
- P 0 \to (\forall n. acc_nat P n \to P (S n)) \to
- \forall n. acc_nat P n.
+theorem wf_le: ∀P. P 0 → (∀n. acc_nat P n → P (S n)) → ∀n. acc_nat P n.
unfold acc_nat; intros 4; elim n names 0; clear n;
[ intros; lapply linear le_n_O_to_eq to H2; destruct; autobatch
| intros 3; elim m; clear m; intros; clear H3;
- [ clear H H1; autobatch
+ [ clear H H1; autobatch depth = 2
| clear H; lapply linear le_inv_S_S to H4;
apply H1; clear H1; intros;
apply H2; clear H2; autobatch depth = 2
].
qed.
-theorem wf_nat_ind: \forall P:nat \to Prop.
- P O \to
- (\forall n. (\forall m. m <= n \to P m) \to P (S n)) \to
- \forall n. P n.
+theorem wf_nat_ind:
+ ∀P:nat→Prop. P O → (∀n. (∀m. m ≤ n → P m) → P (S n)) → ∀n. P n.
intros; lapply linear depth=2 wf_le to H, H1 as H0;
- unfold acc_nat in H0; apply (H0 n n); autobatch.
+ unfold acc_nat in H0; apply (H0 n n); autobatch depth = 1.
qed.
include "preamble.ma".
-(* ACZEL CATEGORIES
+(* CLASSES:
- We use typoids with a compatible membership relation
- The category is intended to be the domain of the membership relation
- The membership relation is necessary because we need to regard the
*)
record Class: Type ≝ {
- class:> Type;
- cin: class → Prop;
- ces: class → class \to Prop
+ class :> Type;
+ cin : class → Prop;
+ ces : class → class → Prop;
+ ces_cin_fw: ∀c1,c2. cin c1 → ces c1 c2 → cin c2;
+ ces_cin_bw: ∀c1,c2. cin c1 → ces c2 c1 → cin c2
}.
-(* default inhabitance predicates *)
-definition true_f ≝ λ(X:Type). λ(_:X). True.
-definition false_f ≝ λ(X:Type). λ(_:X). False.
+(* equality predicate *******************************************************)
-(* equality predicate *)
inductive ceq (C:Class): class C → class C → Prop ≝
- | ceq_refl : ∀c. cin ? c → ceq ? c c
- | ceq_trans: ∀c1,c,c2. cin ? c1 → ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
- | ceq_conf : ∀c1,c,c2. cin ? c1 → ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
+ | ceq_refl : ∀c. ceq ? c c
+ | ceq_trans: ∀c1,c,c2. ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
+ | ceq_conf : ∀c1,c,c2. ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
.
+(* default inhabitance predicates *******************************************)
+
+definition true_f ≝ λX:Type. λ_:X. True.
+
+definition false_f ≝ λX:Type. λ_:X. False.
+
+(* default foreward compatibilities *****************************************)
+
+theorem const_fw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x1 x2 → A.
+intros; autobatch.
+qed.
+
+definition true_fw ≝ const_fw True.
+
+definition false_fw ≝ const_fw False.
+
+(* default backward compatibilities *****************************************)
+
+theorem const_bw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x2 x1 → A.
+intros; autobatch.
+qed.
+
+definition true_bw ≝ const_bw True.
+
+definition false_bw ≝ const_bw False.
include "Class/defs.ma".
-(* ACZEL CATEGORIES:
+(* CLASSES:
- Here we prove the standard properties of the equality.
*)
-theorem ceq_cin_sx: ∀C,c1,c2. ceq C c1 c2 → cin ? c1.
-intros; elim H; clear H c1 c2; autobatch.
+theorem ceq_cin_fw: ∀C,c1,c2. ceq C c1 c2 → cin ? c1 → cin ? c2.
+intros 4; elim H; clear H c1 c2; autobatch.
qed.
-theorem ceq_cin_dx: ∀C,c1,c2. ceq C c1 c2 → cin ? c2.
-intros; elim H; clear H c1 c2; autobatch.
+theorem ceq_cin_bw: ∀C,c1,c2. ceq C c1 c2 → cin ? c2 → cin ? c1.
+intros 4; elim H; clear H c1 c2; autobatch.
qed.
theorem ceq_trans: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c2 c3 → ceq ? c1 c3.
intros 4; elim H; clear H c1 c2; autobatch.
qed.
-theorem ceq_conf: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c1 c3 → ceq ? c2 c3.
-intros 4; elim H; clear H c1 c2; autobatch depth = 4.
+theorem ceq_sym: ∀ C,c1,c2. ceq C c1 c2 → ceq ? c2 c1.
+intros; elim H; clear H c1 c2; autobatch.
qed.
-theorem ceq_sym: ∀ C,c1,c2. ceq C c1 c2 → ceq ? c2 c1.
-intros; autobatch depth = 4.
+theorem ceq_conf: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c1 c3 → ceq ? c2 c3.
+intros; autobatch.
qed.
theorem ceq_repl: ∀C,c1,c2. ceq C c1 c2 →
- ∀d1. ceq ? c1 d1 → ∀d2. ceq ? c2 d2 → ceq ? d1 d2.
+ ∀d1. ceq ? c1 d1 → ∀d2. ceq ? c2 d2 → ceq ? d1 d2.
intros; autobatch.
qed.
*)
definition DBool: Domain ≝
- mk_Domain (mk_Class bool (true_f ?) (eq ?)).
+ mk_Domain (
+ mk_Class bool (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
+ ).
(*
definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def
\lambda C,c0,c1,b.
].
*)
definition DVoid: Domain ≝
- mk_Domain (mk_Class void (true_f ?) (eq ?)).
+ mk_Domain (
+ mk_Class void (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
+ ).
(*
definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def
\lambda C,v.
include "Domain/defs.ma".
(* SUBSETS
- - We use predicative subsets coded as propositional functions
- according to G.Sambin and S.Valentini "Toolbox".
+ - We use predicative subsets encoded as propositional functions
+ according to Sambin/Valentini "Toolbox".
*)
-definition Subset ≝ λD:Domain. D → Prop.
+record Subset (D:Domain): Type ≝ {
+ subset :1> D → Prop;
+ ces_subset_fw: ∀d1,d2. subset d1 → ces ? d1 d2 → subset d2;
+ ces_subset_bw: ∀d1,d2. subset d1 → ces ? d2 d1 → subset d2
+}.
-(* subset membership (epsilon) *)
-definition sin : ∀D. Subset D → D → Prop ≝
- λD:Domain. λU,d. cin D d ∧ U d.
+(* subset membership (epsilon) ********************************************)
-(* subset top (full subset) *)
-definition stop ≝ λD:Domain. true_f D.
+definition sin: ∀D. Subset D → D → Prop ≝
+ λD. λU:Subset D. λd. cin D d ∧ U d.
-coercion stop.
+theorem sin_i: ∀D. ∀U:Subset D. ∀d. cin D d → U d → sin ? U d.
+ unfold sin; intros; autobatch.
+qed.
-(* subset bottom (empty subset) *)
-definition sbot ≝ λD:Domain. false_f D.
+theorem sin_e1: ∀D. ∀U:Subset D. ∀d. sin ? U d → cin D d.
+ intros; decompose; autobatch.
+qed.
+
+theorem sin_e2: ∀D. ∀U:Subset D. ∀d. sin ? U d → U d.
+ intros; decompose; autobatch.
+qed.
+
+(* the domain built upon a subset *****************************************)
+
+theorem ces_sin_fw: ∀D,U,d1,d2. sin D U d1 → ces ? d1 d2 → sin D U d2.
+ intros;
+ apply sin_i;
+ [ autobatch
+ | apply (ces_subset_fw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
+ ].
+qed.
+
+theorem ces_sin_bw: ∀D,U,d1,d2. sin D U d1 → ces ? d2 d1 → sin D U d2.
+ intros;
+ apply sin_i;
+ [ autobatch
+ | apply (ces_subset_bw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
+ ].
+qed.
+
+definition domain_of_subset: ∀D. Subset D → Domain ≝
+ λD:Domain. λU.
+ mk_Domain (mk_Class D (sin D U) (ces D) (ces_sin_fw ? ?) (ces_sin_bw ? ?)).
+
+coercion domain_of_subset.
+
+(* subset top (full subset) ***********************************************)
+
+definition stop: ∀D. Subset D ≝
+ λD. mk_Subset D (true_f ?) (true_fw ? ?) (true_bw ? ?).
+
+coercion stop nocomposites.
+
+(* subset bottom (empty subset) *******************************************)
+
+definition sbot: ∀D. Subset D ≝
+ λD. mk_Subset D (false_f ?) (false_fw ? ?) (false_bw ? ?).
+
+(* subset and (binary intersection) ***************************************)
+
+theorem ces_sand_fw:
+ ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d1 d2 → U1 d2 ∧ U2 d2.
+ intros; decompose; apply conj;
+ [ apply (ces_subset_fw D U1 d1); autobatch (**)
+ | apply (ces_subset_fw D U2 d1); autobatch
+ ].
+qed.
+
+theorem ces_sand_bw:
+ ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d2 d1 → U1 d2 ∧ U2 d2.
+ intros; decompose; apply conj;
+ [ apply (ces_subset_bw D U1 d1); autobatch (**)
+ | apply (ces_subset_bw D U2 d1); autobatch
+ ].
+qed.
-(* subset and (binary intersection) *)
definition sand: ∀D. Subset D → Subset D → Subset D ≝
- λD,U1,U2,d. U1 d ∧ U2 d.
+ λD,U1,U2.
+ mk_Subset D (λd. U1 d ∧ U2 d) (ces_sand_fw ? U1 U2) (ces_sand_bw ? U1 U2).
+
+(* subset or (binary union) ***********************************************)
+
+theorem ces_sor_fw:
+ ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d1 d2 → U1 d2 ∨ U2 d2.
+ intros; decompose;
+ [ apply or_introl; apply (ces_subset_fw D U1 d1); autobatch (**)
+ | apply or_intror; apply (ces_subset_fw D U2 d1); autobatch
+ ].
+qed.
+
+theorem ces_sor_bw:
+ ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d2 d1 → U1 d2 ∨ U2 d2.
+ intros; decompose;
+ [ apply or_introl; apply (ces_subset_bw D U1 d1); autobatch (**)
+ | apply or_intror; apply (ces_subset_bw D U2 d1); autobatch
+ ].
+qed.
-(* subset or (binary union) *)
definition sor: ∀D. Subset D → Subset D → Subset D ≝
- λD,U1,U2,d. U1 d ∨ U2 d.
+ λD,U1,U2.
+ mk_Subset D (λd. U1 d ∨ U2 d) (ces_sor_fw ? U1 U2) (ces_sor_bw ? U1 U2).
+
+(* subset less or equal (inclusion) ***************************************)
-(* subset less or equal (inclusion) *)
definition sle: ∀D. Subset D → Subset D → Prop ≝
- λD,U1,U2. \iforall d. U1 d → U2 d.
+ λD. λU1,U2:Subset D. \iforall d. U1 d → U2 d.
+
+(* subset overlap *********************************************************)
-(* subset overlap *)
definition sover: ∀D. Subset D → Subset D → Prop ≝
- λD,U1,U2. \iexists d. U1 d ∧ U2 d.
+ λD. λU1,U2:Subset D. \iexists d. U1 d ∧ U2 d.
-(* the class of the subsets of a domain *)
-definition subsets_of_domain ≝
- λD. mk_Class (Subset D) (true_f ?) (sle ?).
+(* the class of the subsets of a domain ***********************************)
-(* the domain built upon a subset *)
-definition domain_of_subset: ∀D. Subset D → Domain ≝
- λD:Domain. λU. mk_Domain (mk_Class D (sin D U) (ces D)).
+definition power: Domain → Class ≝
+ λD. mk_Class (Subset D) (true_f ?) (sle ?) (true_fw ? ?) (true_bw ? ?).
projects / helm.git / commitdiff