alias symbol "eq" = "setoid eq".
alias symbol "eq" = "setoid1 eq".
alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
-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;
naxiom ad_hoc16: ∀a,b,c. a < c → a < b + c.
naxiom not_lt_to_le: ∀a,b. ¬ (a < b) → b ≤ a.
naxiom le_to_le_S_S: ∀a,b. a ≤ b → S a ≤ S b.
-naxiom minus_S_S: ∀a,b. S a - S b = a - b.
naxiom minus_S: ∀n. S n - n = S O.
naxiom ad_hoc17: ∀a,b,c,d,d'. a+c+d=b+c+d' → a+d=b+d'.
naxiom split_big_plus:
fst … p ≤ n ∧ snd … p < s (fst … p).
#n; #s; nelim n
[ #m; nwhd in ⊢ (??% → let p ≝ % in ?); nwhd in ⊢ (??(??%) → ?);
- nrewrite > (plus_n_O (s O)); #H; nrewrite > (ltb_t … H); nnormalize;
- napply conj [ napply conj [ napply refl | napply le_n ] ##| nassumption ]
+ nrewrite > (plus_n_O (s O)); #H; nrewrite > (ltb_t … H); nnormalize; @
+ [ @ [ napply refl | napply le_n ] ##| nassumption ]
##| #n'; #Hrec; #m; nwhd in ⊢ (??% → let p ≝ % in ?); #H;
ncases (ltb_cases m (s (S n'))); *; #H1; #H2; nrewrite > H2;
nwhd in ⊢ (let p ≝ % in ?); nwhd
| nnormalize; napply le_n]
##| nnormalize; nassumption ]
##| nchange in H with (m < s (S n') + big_plus (S n') (λi.λ_.s i));
- ngeneralize in match (Hrec (m - s (S n')) ?) in ⊢ ?
- [##2: napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; napply conj
+ nlapply (Hrec (m - s (S n')) ?)
+ [ napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; @
[##2: nassumption
- |napply conj
+ |@
[nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip]
nrewrite > (ad_hoc12 …); ##[##2: nassumption]
nwhd in ⊢ (????(?(??%)?));
∀A. ∀P:partition A. ∀n,s.
∀f:isomorphism ?? (Nat_ n) (indexes ? P).
(∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) →
- (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) (Full_set A)).
- STOP #A; #P; #Sn; ncases Sn
- [ #s; #f; #fi;
- ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #H;
+ (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) A).
+ #A; #P; #Sn; ncases Sn
+ [ #s; #f; #fi; nlapply (covers ? P); *; #_; #H;
(*
- ngeneralize in match
- (big_union_preserves_iso ??? (indexes A P) (Nat_ O) (λx.class ? P x) f) in ⊢ ?;
+ nlapply
+ (big_union_preserves_iso ??? (indexes A P) (Nat_ O) (λx.class ? P x) f);
*; #K; #_; nwhd in K: (? → ? → %);*)
nelim daemon (* impossibile *)
- | #n; #s; #f; #fi; napply mk_isomorphism
- [ napply mk_unary_morphism
+ | #n; #s; #f; #fi; @
+ [ @
[ napply (λm.let p ≝ iso_nat_nat_union s m n in iso_f ???? (fi (fst … p)) (snd … p))
| #a; #a'; #H; nrewrite < H; napply refl ]
##| #x; #Hx; nwhd; napply I