From: Enrico Tassi Date: Mon, 20 Oct 2008 08:12:43 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~4658 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1ee5193677b8e2a80d4f068ee79ecac335de1196;p=helm.git ... --- diff --git a/helm/software/components/ng_kernel/TODO b/helm/software/components/ng_kernel/TODO index cfe8ca117..02913a155 100644 --- a/helm/software/components/ng_kernel/TODO +++ b/helm/software/components/ng_kernel/TODO @@ -13,6 +13,8 @@ e la si tagga con bound a seconda del test_eq_only <= k. nel vecchio nucleo la height_of di un b-redex fa 0 e quindi riduci in forma normale. Spostare la small_delta_step. + +@ tra universi senza duplicati ------- ?1 = t (?1,?2)::(?2,t)::subst diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 496ae5446..0ddd3601d 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -51,6 +51,8 @@ let pp_constraints () = String.concat "\n" (List.map (fun (b,x,y) -> pp_constraint b x y) !le_constraints) ;; +let universes = ref [];; + let add_constraint strict a b = match a,b with | [false,a2],[false,b2] -> @@ -58,11 +60,30 @@ let add_constraint strict a b = if le_path_uri [] (not strict) b2 a2 then (raise(BadConstraint(lazy("universe inconsistency adding "^pp_constraint strict a2 b2 ^ " to:\n" ^ pp_constraints ())))); + universes := a2 :: b2 :: + List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes; le_constraints := (strict,a2,b2) :: !le_constraints) | _ -> raise (BadConstraint (lazy "trying to add a constraint on an inferred universe")) ;; +let sup l = + match l with + | [false,_] -> Some l + | l -> + let bigger_than acc (s1,n1) = List.filter (le_path_uri [] s1 n1) acc in + let solutions = List.fold_left bigger_than !universes l in + let rec aux = function + | [] -> None + | u :: tl -> + if List.exists (fun x -> le_path_uri [] true x u) solutions then aux tl + else Some [false,u] + in + aux solutions +;; + + + let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;; let set_typecheck_obj f = if !already_set then diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 029cd94d1..758b44be9 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -29,6 +29,7 @@ val universe_leq: NCic.universe -> NCic.universe -> bool true -> strict check (<); false -> loose check (<=) *) val add_constraint: bool -> NCic.universe -> NCic.universe -> unit +val sup : NCic.universe -> NCic.universe option val pp_constraints: unit -> string val get_checked_def: diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt index 42a02ebf1..863921720 100644 --- a/helm/software/components/ng_refiner/.depend.opt +++ b/helm/software/components/ng_refiner/.depend.opt @@ -4,5 +4,5 @@ nCicMetaSubst.cmo: nCicMetaSubst.cmi nCicMetaSubst.cmx: nCicMetaSubst.cmi nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi -nCicRefiner.cmo: nCicRefiner.cmi -nCicRefiner.cmx: nCicRefiner.cmi +nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi +nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicRefiner.cmi diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index 3b951bec2..bc22a2160 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -169,6 +169,17 @@ let _ = in prerr_endline "ranked...."; prerr_endline (NCicEnvironment.pp_constraints ()); +(* + let [_,type0_uri] = mk_type 0 in + let [_,type1_uri] = mk_type 1 in + let [_,type2_uri] = mk_type 2 in + prerr_endline + ("Min:" ^ + (match NCicEnvironment.sup [true,type0_uri;true,type2_uri] with + | None -> "NO SUP" + | Some t -> NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] + (NCic.Sort (NCic.Type t)))); +*) HExtlib.profiling_enabled := false; List.iter (fun uu -> let uu= OCic2NCic.nuri_of_ouri uu in diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 10eff13b4..253af6f37 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -94,29 +94,33 @@ let check_allowed_sort_elimination localise r orig = let rec aux metasenv subst context ind arity1 arity2 = (*D*)inside 'S'; try let rc = let arity1 = NCicReduction.whd ~subst context arity1 in + pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ " ... " ^ + NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nNEV:"^ +NCicPp.ppmetasenv ~subst metasenv +)); match arity1 with | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) -> let metasenv, meta, _ = - NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Typeless + NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type in let metasenv, subst = try NCicUnification.unify metasenv subst context - (C.Prod (name, so1, meta)) arity2 + arity2 (C.Prod (name, so1, meta)) with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf "expected %s, found %s" (* XXX localizzare meglio *) - (NCicPp.ppterm ~subst ~metasenv ~context arity1) + (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod (name, so1, meta))) (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc) in aux metasenv subst ((name, C.Decl so1)::context) (mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta | C.Sort _ (* , t ==?== C.Prod _ *) -> - let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Typeless in + let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in let metasenv, subst = try NCicUnification.unify metasenv subst context - (C.Prod ("_", ind, meta)) arity2 + arity2 (C.Prod ("_", ind, meta)) with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf "expected %s, found %s" (* XXX localizzare meglio *) - (NCicPp.ppterm ~subst ~metasenv ~context arity1) + (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod ("_", ind, meta))) (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc) in (try NCicTypeChecker.check_allowed_sort_elimination diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 24ab7b4af..d3c86d281 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -72,13 +72,23 @@ let indent = ref "";; let inside c = indent := !indent ^ String.make 1 c;; let outside () = indent := String.sub !indent 0 (String.length !indent -1);; -(* let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; -*) -let pp _ = ();; +(* let pp _ = ();; *) + +let fix_sorts metasenv subst context meta t = + let rec aux () = function + | NCic.Sort (NCic.Type u) as orig -> + (match NCicEnvironment.sup u with + | None -> raise (fail_exc metasenv subst context meta t) + | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)) + | NCic.Meta _ as orig -> orig + | t -> NCicUtils.map (fun _ _ -> ()) () aux t + in + aux () t +;; let rec beta_expand num test_eq_only swap metasenv subst context t arg = let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' = @@ -142,28 +152,44 @@ and beta_expand_many test_equality_only swap metasenv subst context t args = (* (*D*) in outside (); rc with exn -> outside (); raise exn *) and instantiate test_eq_only metasenv subst context n lc t swap = -(* (*D*) inside 'I'; try let rc = *) + (*D*) inside 'I'; try let rc = let unify test_eq_only m s c t1 t2 = if swap then unify test_eq_only m s c t2 t1 else unify test_eq_only m s c t1 t2 in + let fix_sorts t = + if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t + else + NCic.Sort (NCic.Type ( + match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ -> + assert false)) + in let name, ctx, ty = NCicUtils.lookup_meta n metasenv in - let metasenv, subst = + let metasenv, subst, t = match ty with - | NCic.Implicit (`Typeof _) -> metasenv, subst + | NCic.Implicit (`Typeof _) -> metasenv, subst, fix_sorts t | _ -> - let lty = NCicSubstitution.subst_meta lc ty in - let ty_t = - try NCicTypeChecker.typeof ~subst ~metasenv context t - with NCicTypeChecker.TypeCheckerFailure msg -> - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); - prerr_endline (Lazy.force msg); - assert false + pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)); + let t, ty_t = + try t, NCicTypeChecker.typeof ~subst ~metasenv context t + with NCicTypeChecker.TypeCheckerFailure _ -> + let ft = fix_sorts t in + if ft == t then assert false else + try + pp (lazy ("typeof: " ^ + NCicPp.ppterm ~metasenv ~subst ~context ft)); + ft, NCicTypeChecker.typeof ~subst ~metasenv context ft + with NCicTypeChecker.TypeCheckerFailure msg -> + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft); + prerr_endline (Lazy.force msg); + assert false in + let lty = NCicSubstitution.subst_meta lc ty in pp (lazy("On the types: " ^ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); - unify test_eq_only metasenv subst context lty ty_t + let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in + metasenv, subst, t in let (metasenv, subst), t = try NCicMetaSubst.delift metasenv subst context n lc t @@ -187,16 +213,14 @@ and instantiate test_eq_only metasenv subst context n lc t swap = List.filter (fun (m,_) -> not (n = m)) metasenv in metasenv, subst -(* (*D*) in outside(); rc with exn -> outside (); raise exn *) + (*D*) in outside(); rc with exn -> outside (); raise exn and unify test_eq_only metasenv subst context t1 t2 = -(* (*D*) inside 'U'; try let rc = *) + (*D*) inside 'U'; try let rc = let fo_unif test_eq_only metasenv subst t1 t2 = -(* (*D*) inside 'F'; try let rc = *) -(* + (*D*) inside 'F'; try let rc = pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context t2)); -*) if t1 === t2 then metasenv, subst else @@ -380,7 +404,7 @@ and unify test_eq_only metasenv subst context t1 t2 = raise (uncert_exc metasenv subst context t1 t2)) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | _ -> raise (uncert_exc metasenv subst context t1 t2) -(* (*D*) in outside(); rc with exn -> outside (); raise exn *) + (*D*) in outside(); rc with exn -> outside (); raise exn in let height_of = function | NCic.Const (Ref.Ref (_,Ref.Def h)) @@ -411,7 +435,7 @@ and unify test_eq_only metasenv subst context t1 t2 = let rec unif_machines metasenv subst = function | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) -> -(* (*D*) inside 'M'; try let rc = *) + (*D*) inside 'M'; try let rc = (* pp (lazy((if are_normal then "*" else " ") ^ " " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^ @@ -446,7 +470,7 @@ and unify test_eq_only metasenv subst context t1 t2 = try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst) with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) -> unif_machines metasenv subst (small_delta_step m1 m2) -(* (*D*) in outside(); rc with exn -> outside (); raise exn *) + (*D*) in outside(); rc with exn -> outside (); raise exn in try fo_unif test_eq_only metasenv subst t1 t2 with UnificationFailure msg | Uncertain msg as exn -> @@ -456,7 +480,7 @@ and unify test_eq_only metasenv subst context t1 t2 = with | UnificationFailure _ -> raise (UnificationFailure msg) | Uncertain _ -> raise exn -(* (*D*) in outside(); rc with exn -> outside (); raise exn *) + (*D*) in outside(); rc with exn -> outside (); raise exn ;; let unify = diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma index 0bc8a3225..e724dc2e6 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma @@ -36,7 +36,7 @@ record ordered_uniform_space : Type ≝ { ous_stuff :> ordered_uniform_space_; ous_convex: ∀U.us_unifbase ous_stuff U → convex ous_stuff U }. - +(* definition Type_of_ordered_uniform_space : ordered_uniform_space → Type. intro; compose ordered_set_OF_ordered_uniform_space with os_l. apply (hos_carr (f o)); @@ -47,9 +47,9 @@ intro; compose ordered_set_OF_ordered_uniform_space with os_r. apply (hos_carr (f o)); qed. -coercion Type_of_ordered_uniform_space. coercion Type_of_ordered_uniform_space_dual. - +coercion Type_of_ordered_uniform_space. +*) definition half_ordered_set_OF_ordered_uniform_space : ordered_uniform_space → half_ordered_set. intro; compose ordered_set_OF_ordered_uniform_space with os_l. apply (f o); qed. @@ -143,39 +143,39 @@ intros (O l r); apply mk_ordered_uniform_space; [1: intros (U H); intro x; simplify; cases H (w Hw); cases Hw (Gw Hwp); clear H Hw; intro Hm; lapply (us_phi1 O w Gw x Hm) as IH; - apply (restrict ? l r ??? Hwp IH); STOP + apply (restrict ? l r ??? Hwp IH); |2: intros (U V HU HV); cases HU (u Hu); cases HV (v Hv); clear HU HV; cases Hu (Gu HuU); cases Hv (Gv HvV); clear Hu Hv; - cases (us_phi2 ??? Gu Gv) (w HW); cases HW (Gw Hw); clear HW; - exists; [apply (λb:{[l,r]} square.w b)] split; + cases (us_phi2 O u v Gu Gv) (w HW); cases HW (Gw Hw); clear HW; + exists; [apply (λb:{[l,r]} squareB.w b)] split; [1: unfold f; simplify; clearbody f; exists; [apply w]; split; [assumption] intro b; simplify; unfold segment_square_of_ordered_set_square; cases b; intros; split; intros; assumption; |2: intros 2 (x Hx); cases (Hw ? Hx); split; - [apply (restrict ?????? HuU H)|apply (restrict ?????? HvV H1);]] + [apply (restrict O l r ??? HuU H)|apply (restrict O l r ??? HvV H1);]] |3: intros (U Hu); cases Hu (u HU); cases HU (Gu HuU); clear Hu HU; - cases (us_phi3 ?? Gu) (w HW); cases HW (Gw Hwu); clear HW; - exists; [apply (λx:{[l,r]} square.w x)] split; + cases (us_phi3 O u Gu) (w HW); cases HW (Gw Hwu); clear HW; + exists; [apply (λx:{[l,r]} squareB.w x)] split; [1: exists;[apply w];split;[assumption] intros; simplify; intro; unfold segment_square_of_ordered_set_square; cases b; intros; split; intro; assumption; - |2: intros 2 (x Hx); apply (restrict ?????? HuU); apply Hwu; + |2: intros 2 (x Hx); apply (restrict O l r ??? HuU); apply Hwu; cases Hx (m Hm); exists[apply (\fst m)] apply Hm;] |4: intros (U HU x); cases HU (u Hu); cases Hu (Gu HuU); clear HU Hu; - cases (us_phi4 ?? Gu x) (Hul Hur); + cases (us_phi4 O u Gu x) (Hul Hur); split; intros; - [1: lapply (invert_restriction_agreement ????? HuU) as Ra; - apply (restrict ????? x Ra); - apply Hul; apply (unrestrict ?????? HuU H); - |2: apply (restrict ?????? HuU); apply Hur; - apply (unrestrict ?????? (invert_restriction_agreement ????? HuU) H);]] + [1: lapply (invert_restriction_agreement O l r ?? HuU) as Ra; + apply (restrict O l r ?? x Ra); + apply Hul; apply (unrestrict O l r ??? HuU H); + |2: apply (restrict O l r ??? HuU); apply Hur; + apply (unrestrict O l r ??? (invert_restriction_agreement O l r ?? HuU) H);]] |2: simplify; reflexivity;] |2: simplify; unfold convex; intros; cases H (u HU); cases HU (Gu HuU); clear HU H; - lapply (ous_convex ?? Gu (bs_of_ss ? l r p) ? H2 (bs_of_ss ? l r y) H3) as Cu; - [1: apply (unrestrict ?????? HuU); apply H1; - |2: apply (restrict ?????? HuU Cu);]] + lapply (ous_convex ?? Gu p ? H2 y H3) as Cu; + [1: apply (unrestrict O l r ??? HuU); apply H1; + |2: apply (restrict O l r ??? HuU Cu);]] qed. interpretation "Ordered uniform space segment" 'segment_set a b = @@ -185,9 +185,10 @@ interpretation "Ordered uniform space segment" 'segment_set a b = alias symbol "pi1" = "exT \fst". lemma restric_uniform_convergence: ∀O:ordered_uniform_space.∀l,u:O. - ∀x:{[l,u]}. - ∀a:sequence {[l,u]}. - ⌊n,\fst (a n)⌋ uniform_converges (\fst x) → + ∀x:(segment_ordered_uniform_space O l u). + ∀a:sequence (segment_ordered_uniform_space O l u). + uniform_converge (segment_ordered_uniform_space O l u) + (mk_seq O (λn:nat.\fst (a n))) (\fst x) → True. a uniform_converges x. intros 8; cases H1; cases H2; clear H2 H1; cases (H ? H3) (m Hm); exists [apply m]; intros; diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index bcf68a660..ae3231d91 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,6 +1,6 @@ +Z/times.ma Z/plus.ma nat/lt_arith.ma list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma -Z/times.ma Z/plus.ma nat/lt_arith.ma nat/factorial.ma nat/le_arith.ma nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma @@ -8,41 +8,41 @@ nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/itera Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma nat/lt_arith.ma nat/div_and_mod.ma nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma +nat/binomial.ma nat/factorial2.ma nat/iteration2.ma Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma nat/euler_theorem.ma nat/map_iter_p.ma nat/nat.ma nat/totient.ma -nat/binomial.ma nat/factorial2.ma nat/iteration2.ma Z/orders.ma Z/z.ma nat/orders.ma datatypes/subsets.ma datatypes/categories.ma logic/cprop_connectives.ma -nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma logic/connectives2.ma higher_order_defs/relations.ma +nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma Q/ratio/rinv.ma Q/fraction/finv.ma Q/ratio/ratio.ma nat/o.ma nat/binomial.ma nat/sqrt.ma -Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma -Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma +Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma nat/plus.ma nat/nat.ma +Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma formal_topology/saturations_reductions.ma datatypes/subsets.ma algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma datatypes/categories.ma logic/cprop_connectives.ma nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma -higher_order_defs/ordering.ma logic/equality.ma -nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma -Q/q.ma Q/fraction/fraction.ma Z/compare.ma Z/plus.ma nat/factorization.ma +nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma +higher_order_defs/ordering.ma logic/equality.ma datatypes/constructors.ma logic/equality.ma +Q/q.ma Q/fraction/fraction.ma Z/compare.ma Z/plus.ma nat/factorization.ma Z/compare.ma Z/orders.ma nat/compare.ma -Q/fraction/numerator_denominator.ma Q/fraction/finv.ma Q/q/q.ma Q/fraction/numerator_denominator.ma Q/ratio/ratio.ma +Q/fraction/numerator_denominator.ma Q/fraction/finv.ma nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma -decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma -Q/ratio/ratio.ma Q/fraction/fraction.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma -nat/div_and_mod_diseq.ma nat/lt_arith.ma nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma -technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma +Q/ratio/ratio.ma Q/fraction/fraction.ma +nat/div_and_mod_diseq.ma nat/lt_arith.ma +decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma logic/connectives.ma +technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma datatypes/compare.ma nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma @@ -50,60 +50,60 @@ nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma nat/factorial2.ma nat/exp.ma nat/factorial.ma nat/chebyshev_thm.ma nat/neper.ma algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma -nat/gcd_properties1.ma nat/gcd.ma demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma +nat/gcd_properties1.ma nat/gcd.ma nat/minimization.ma nat/minus.ma decidable_kit/fgraph.ma decidable_kit/fintype.ma -formal_topology/formal_topologies.ma formal_topology/basic_topologies.ma formal_topology/relations.ma datatypes/subsets.ma +formal_topology/formal_topologies.ma formal_topology/basic_topologies.ma Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma Z/plus.ma Z/z.ma nat/minus.ma -Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma -nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma nat/minus.ma nat/compare.ma nat/le_arith.ma -formal_topology/concrete_spaces.ma formal_topology/basic_pairs.ma +nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma +Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma Z/z.ma datatypes/bool.ma nat/nat.ma +formal_topology/concrete_spaces.ma formal_topology/basic_pairs.ma decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma nat/map_iter_p.ma nat/count.ma nat/permutation.ma -decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma demo/realisability.ma datatypes/constructors.ma logic/connectives.ma nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma +decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma nat/gcd.ma nat/lt_arith.ma nat/primes.ma nat/factorization.ma nat/ord.ma -decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma algebra/monoids.ma algebra/semigroups.ma -logic/coimplication.ma logic/connectives.ma demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma -higher_order_defs/functions.ma logic/equality.ma +logic/coimplication.ma logic/connectives.ma +decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma +higher_order_defs/functions.ma logic/equality.ma algebra/semigroups.ma higher_order_defs/functions.ma -Q/nat_fact/times.ma nat/factorization.ma -nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma nat/sieve.ma list/sort.ma nat/primes.ma +nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma +Q/nat_fact/times.ma nat/factorization.ma nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma -higher_order_defs/relations.ma logic/connectives.ma -nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma logic/cprop_connectives.ma logic/connectives.ma +nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma +higher_order_defs/relations.ma logic/connectives.ma demo/toolbox.ma logic/cprop_connectives.ma -Q/inv.ma Q/q/q.ma Q/fraction/finv.ma Q/q.ma demo/natural_deduction.ma +Q/inv.ma Q/q/q.ma Q/fraction/finv.ma Q/q.ma decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma Z/moebius.ma Z/sigma_p.ma nat/factorization.ma Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma -Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/nat.ma nat/factorization.ma Q/fraction/ftimes.ma Q/fraction/finv.ma Q/nat_fact/times.ma Q/ratio/ratio.ma Z/times.ma Q/q/qplus.ma nat/factorization.ma +Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/nat.ma nat/factorization.ma Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sieve.ma nat/sqrt.ma nat/nat.ma higher_order_defs/functions.ma formal_topology/basic_topologies.ma datatypes/categories.ma formal_topology/relations.ma formal_topology/saturations_reductions.ma nat/chebyshev.ma nat/o.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma +demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma nat/congruence.ma nat/primes.ma nat/relevant_equations.ma nat/le_arith.ma nat/orders.ma nat/times.ma -demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma nat/times.ma nat/plus.ma formal_topology/basic_pairs.ma datatypes/categories.ma formal_topology/relations.ma list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma -nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma +nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma