From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 9 Jul 2008 11:19:02 +0000 (+0000)
Subject: CProp hierarchy fixed:
X-Git-Tag: make_still_working~4950
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4d765cc85e3a1e84c80c348a1e67ea1eed984916;p=helm.git

CProp hierarchy fixed:
- CProp universes are not swept away
- CProp i : Type j (where i < j, used to be a fresh j)
- new kernel universe inconsistency error message improved
- pp function for universes constraints for new kernel

Formal topology example fixed to eploit left parameters to reduce the universe
height and solve universe inconsistency
---

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index fa773a4db..cf6b6eeff 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -474,8 +474,14 @@ let add_eq u v b =
 let rank = ref MAL.empty;;
 
 let do_rank (b,_,_) =
-(*         print_ugraph ugraph; *)
-   let keys = MAL.fold (fun k _ acc -> k::acc) b [] in
+   let keys = 
+     MAL.fold 
+       (fun k v acc -> 
+          SOF.union acc (SOF.union (SOF.singleton k) 
+            (SOF.union v.eq_closure (SOF.union v.gt_closure v.ge_closure))))
+       b SOF.empty 
+   in
+   let keys = SOF.elements keys in
    let fall =
      List.fold_left 
        (fun acc u ->
@@ -483,7 +489,6 @@ let do_rank (b,_,_) =
            | [] -> 0, seen
            | x::tl when SOF.mem x seen -> aux k seen tl
            | x::tl ->
-(*                prerr_endline (String.make k '.' ^ string_of_universe x); *)
                let seen = SOF.add x seen in
                let t1, seen = aux (k+1) seen (SOF.elements (repr x b).eq_closure) in
                let t3, seen = aux (k+1) seen (SOF.elements (repr x b).gt_closure) in
diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index e3d9add62..cf3a3c49c 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1367,6 +1367,13 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           in
             ((CicSubstitution.subst_meta l ty),ugraph1))
       (* TASSI: CONSTRAINTS *)
+    | C.Sort (C.CProp t) -> 
+       let t' = CicUniv.fresh() in
+       (try
+         let ugraph1 = CicUniv.add_gt t' t ugraph in
+           (C.Sort (C.Type t')),ugraph1
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in
        (try
@@ -1374,7 +1381,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
            (C.Sort (C.Type t')),ugraph1
         with
          CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
-    | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
+    | C.Sort (C.Prop|C.Set) -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
     | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
     | C.Cast (te,ty) as t ->
        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
diff --git a/helm/software/components/cic_proof_checking/cicUnivUtils.ml b/helm/software/components/cic_proof_checking/cicUnivUtils.ml
index 948b26ff0..2c35ebe1a 100644
--- a/helm/software/components/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/software/components/cic_proof_checking/cicUnivUtils.ml
@@ -79,6 +79,8 @@ let universes_of_obj uri t =
     | C.Meta (n,l1) -> C.Meta (n, List.map (HExtlib.map_option aux) l1)
     | C.Sort (C.Type i) -> add_result [i]; 
       C.Sort (C.Type (CicUniv.name_universe i uri))
+    | C.Sort (C.CProp i) -> add_result [i]; 
+      C.Sort (C.CProp (CicUniv.name_universe i uri))
     | C.Rel _ 
     | C.Sort _
     | C.Implicit _ as x -> x
diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 8fa6963aa..fc9dc840d 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -386,7 +386,14 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                  t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
               with
                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
-        | C.Sort _ -> 
+        | C.Sort (C.CProp tno) -> 
+            let tno' = CicUniv.fresh() in 
+             (try
+               let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+                 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | C.Sort (C.Prop|C.Set) -> 
             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
         | C.Implicit infos ->
            let metasenv',t' = exp_impl metasenv subst context infos in
diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 71ba8ddc2..d6165d9db 100644
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -143,32 +143,38 @@ let _ =
     roots_alluris;
   prerr_endline "finished....";
   let lll = List.sort compare (CicUniv.do_rank (get_graph ())) in
-  prerr_endline "caching objects";
   let _ = 
+    try
     let rec aux = function
       | a::(b::_ as tl) ->
          NCicEnvironment.add_constraint true (mk_type a) (mk_type b);
          NCicEnvironment.add_constraint true (mk_cprop a) (mk_cprop b);
          NCicEnvironment.add_constraint true (mk_type a) (mk_cprop a);
          NCicEnvironment.add_constraint true (mk_cprop a) (mk_type b);
-         NCicEnvironment.add_constraint true (mk_type b) (mk_cprop b);
          aux tl
+      | [a] -> 
+         NCicEnvironment.add_constraint true (mk_type a) (mk_cprop a);
       | _ -> ()
     in
        aux lll
+    with NCicEnvironment.BadConstraint s as e ->
+      prerr_endline (Lazy.force s); raise e
   in
   prerr_endline "ranked....";
+  prerr_endline (NCicEnvironment.pp_constraints ());
   HExtlib.profiling_enabled := false;
   List.iter (fun uu ->
     let uu= OCic2NCic.nuri_of_ouri uu in
     indent := 0;
     let o = NCicLibrary.get_obj uu in
+(*       prerr_endline (NCicPp.ppobj o); *)
     try 
       NCicTypeChecker.typecheck_obj o
     with 
     | NCicTypeChecker.AssertFailure s 
     | NCicTypeChecker.TypeCheckerFailure s
     | NCicEnvironment.ObjectNotFound s
+    | NCicEnvironment.BadConstraint s
     | NCicEnvironment.BadDependency s as e -> 
        prerr_endline ("######### " ^ Lazy.force s);
        if not ignore_exc then raise e
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 57f130546..496ae5446 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -43,12 +43,21 @@ let universe_leq a b =
 
 let universe_eq a b = universe_leq b a && universe_leq a b
 
+let pp_constraint b x y =  
+  NUri.name_of_uri x ^ (if b then " < " else " <= ") ^ NUri.name_of_uri y
+;;
+
+let pp_constraints () =
+  String.concat "\n" (List.map (fun (b,x,y) -> pp_constraint b x y) !le_constraints)
+;;
+
 let add_constraint strict a b = 
   match a,b with
   | [false,a2],[false,b2] -> 
       if not (le_path_uri [] strict a2 b2) then (
         if le_path_uri [] (not strict) b2 a2 then
-         (raise (BadConstraint (lazy "universe inconsistency")));
+         (raise(BadConstraint(lazy("universe inconsistency adding "^pp_constraint strict a2 b2
+           ^ " to:\n" ^ pp_constraints ()))));
         le_constraints := (strict,a2,b2) :: !le_constraints)
   | _ -> raise (BadConstraint
           (lazy "trying to add a constraint on an inferred universe"))
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 67b3857d1..029cd94d1 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 pp_constraints: unit -> string
 
 val get_checked_def:
   NReference.reference -> 
diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 50671aa41..05711b7b6 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -44,16 +44,17 @@ record axiom_set : Type ≝
    C: ∀a:A. i a → 2 \sup A
  }.
 
+inductive iter (A: axiom_set) (U,V: 2 \sup A) (covers: A → CProp) : CProp ≝
+   cycle: (∀a:A.a ∈ V → covers a) → iter A U V covers.
+
 inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
    refl: ∀a:A. a ∈ U → covers A U a
- | infinity: ∀a:A. ∀j: i ? a. coversl A U (C ? a j) → covers A U a
-with coversl : (2 \sup A) → CProp ≝
-   iter: ∀V:2 \sup A.(∀a:A.a ∈ V → covers A U a) → coversl A U V.
+ | infinity: ∀a:A. ∀j: i ? a. iter A U (C ? a j) (covers A U) → covers A U a.
 
 notation "hvbox(a break ◃ b)" non associative with precedence 45
 for @{ 'covers $a $b }.
 
-interpretation "coversl" 'covers A U = (coversl _ U A).
+interpretation "coversl" 'covers A U = (iter _ U A (covers _ U)).
 interpretation "covers" 'covers a U = (covers _ U a).
 
 definition covers_elim ≝
@@ -63,11 +64,10 @@ definition covers_elim ≝
     let rec aux (a:A) (p:a ◃ U) on p : a ∈ P ≝
      match p return λaa.λ_:aa ◃ U.aa ∈ P with
       [ refl a q ⇒ H1 a q
-      | infinity a j q ⇒ H2 a j q (auxl (C ? a j) q)
-      ]
-    and auxl (V: 2 \sup A) (q: V ◃ U) on q : ∀b. b ∈ V → b ∈ P ≝
-     match q return λVV.λ_:VV ◃ U.∀b. b ∈ VV → b ∈ P with
-      [ iter VV f ⇒ λb.λr. aux b (f b r) ]
+      | infinity a j q ⇒
+         H2 a j q
+          match q return λ_:(C ? a j) ◃ U.∀b. b ∈ (C ? a j) → b ∈ P with
+          [ cycle f ⇒ λb.λr. aux b (f b r) ]]
     in
      aux.
 
@@ -136,8 +136,8 @@ qed.
 
 theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
  intros;
- generalize in match H; clear H; generalize in match V; clear V;
- apply (covers_elim ?? (mk_powerset A (λa.∀p:2 \sup A.a ⋉ p → U ⋉ p)) ??? H1);
+ generalize in match H; clear H; 
+ apply (covers_elim ?? (mk_powerset A (λa.a ⋉ V → U ⋉ V)) ??? H1);
  clear H1; simplify; intros;
   [ exists [apply a1]
     split;
diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index 3b068389d..bd27126af 100644
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -14,84 +14,85 @@ algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/
 algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma
 algebra/semigroups.ma higher_order_defs/functions.ma
 algebra/monoids.ma algebra/semigroups.ma
+demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma
 demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma
 demo/realisability.ma datatypes/constructors.ma logic/connectives.ma
-demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma
-list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
+demo/formal_topology.ma logic/equality.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
+list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
 logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma
 logic/connectives.ma 
 logic/coimplication.ma logic/connectives.ma
 logic/connectives2.ma higher_order_defs/relations.ma
-nat/sieve.ma list/sort.ma nat/primes.ma
 nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma
 nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma
-nat/factorial2.ma nat/exp.ma nat/factorial.ma
 nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
 nat/congruence.ma nat/primes.ma nat/relevant_equations.ma
 nat/minus.ma nat/compare.ma nat/le_arith.ma
-nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/o.ma nat/pi_p.ma
 nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
 nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma
 nat/factorial.ma nat/le_arith.ma
 nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma
-nat/binomial.ma nat/factorial2.ma nat/iteration2.ma
-nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma
 nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
 nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma
 nat/minimization.ma nat/minus.ma
 nat/gcd.ma nat/lt_arith.ma nat/primes.ma
-nat/chebyshev_thm.ma nat/neper.ma
-nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma
 nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma
 nat/le_arith.ma nat/orders.ma nat/times.ma
-nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma
 nat/times.ma nat/plus.ma
-nat/div_and_mod_diseq.ma nat/lt_arith.ma
-nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma
 nat/gcd_properties1.ma nat/gcd.ma
 nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma
 nat/lt_arith.ma nat/div_and_mod.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/factorization.ma nat/ord.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
+nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma
 nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
+nat/factorial2.ma nat/exp.ma nat/factorial.ma
+nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma
 nat/nat.ma higher_order_defs/functions.ma
 nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma
 nat/map_iter_p.ma nat/count.ma nat/permutation.ma
 nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma
-nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma
 nat/plus.ma nat/nat.ma
-nat/factorization2.ma nat/factorization.ma
 nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma
 nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma
 nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma
 nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma
+nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/o.ma nat/pi_p.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
+nat/chebyshev_thm.ma nat/neper.ma
+nat/div_and_mod_diseq.ma nat/lt_arith.ma
+nat/binomial.ma nat/factorial2.ma nat/iteration2.ma
+nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma
+nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma
+nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma
 nat/o.ma nat/binomial.ma nat/sqrt.ma
-Q/inv.ma Q/q.ma
-Q/frac.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/sieve.ma list/sort.ma nat/primes.ma
+nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma
+Q/q.ma Q/fraction/fraction.ma Z/compare.ma Z/plus.ma nat/factorization.ma
 Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
-Q/q.ma Z/compare.ma Z/plus.ma nat/factorization.ma
-Q/nat_fact/times.ma nat/factorization.ma
+Q/frac.ma nat/nat.ma Q/q/q.ma Q/q/qinv.ma nat/factorization.ma
+Q/inv.ma Q/fraction/finv.ma Q/q.ma Q/q/q.ma
 Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma
 Q/ratio/ratio.ma Q/fraction/fraction.ma
 Q/ratio/rinv.ma Q/fraction/finv.ma Q/ratio/ratio.ma
-Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma
-Q/q/qplus.ma nat/factorization.ma
-Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma
-Q/q/q.ma Q/fraction/numerator_denominator.ma Q/ratio/ratio.ma
+Q/fraction/fraction.ma Z/compare.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/fraction/numerator_denominator.ma Q/fraction/finv.ma
 Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma
-Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma
+Q/q/qplus.ma nat/factorization.ma
+Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma
+Q/q/q.ma Q/fraction/numerator_denominator.ma Q/ratio/ratio.ma
+Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma
+Q/nat_fact/times.ma nat/factorization.ma
 technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma
 decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma
 decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma
-decidable_kit/fgraph.ma decidable_kit/fintype.ma
 decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma
 decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma
 decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma
+decidable_kit/fgraph.ma decidable_kit/fintype.ma
 higher_order_defs/relations.ma logic/connectives.ma
 higher_order_defs/functions.ma logic/equality.ma
 higher_order_defs/ordering.ma logic/equality.ma