atoms of the input goals *)
exception Proved of NTacStatus.tac_status
+let height_of_ref (NReference.Ref (uri, x)) =
+ match x with
+ | NReference.Decl
+ | NReference.Ind _
+ | NReference.Con _
+ | NReference.CoFix _ ->
+ let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in
+ height
+ | NReference.Def h -> h
+ | NReference.Fix (_,_,h) -> h
+;;
+
+let fast_height_of_term t =
+ let h = ref 0 in
+ let rec aux =
+ function
+ NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
+ | NCic.Meta _ -> ()
+ | NCic.Rel _
+ | NCic.Sort _ -> ()
+ | NCic.Implicit _ -> assert false
+ | NCic.Const nref as t ->
+(*
+ prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[]
+ ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref));
+*)
+ h := max !h (height_of_ref nref)
+ | NCic.Prod (_,t1,t2)
+ | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
+ | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
+ | NCic.Appl l -> List.iter aux l
+ | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
+ in
+ aux t; !h
+;;
+
+let height_of_goals status =
+ let open_goals = head_goals status#stack in
+ assert (List.length open_goals > 0);
+ let h = ref 0 in
+ List.iter
+ (fun open_goal ->
+ let ty = get_goalty status open_goal in
+ let context = ctx_of ty in
+ let _, ty = term_of_cic_term status ty (ctx_of ty) in
+ h := max !h (fast_height_of_term ty);
+ List.iter
+ (function
+ | _, NCic.Decl ty -> h := max !h (fast_height_of_term ty)
+ | _, NCic.Def (bo,ty) ->
+ h := max !h (fast_height_of_term ty);
+ h := max !h (fast_height_of_term bo);
+ )
+ context)
+ open_goals;
+ prerr_endline ("altezza sequente: " ^ string_of_int !h);
+ !h
+;;
+
(* let close_failures _ c = c;; *)
(* let prunable _ _ _ = false;; *)
(* let cache_examine cache gty = `Notfound;; *)
unit_eq = unit_eq
}
-let only _ _ _ = true;;
+let only signature _context candidate =
+ (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
+ let candidate_ty =
+ NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
+ in
+ let height = fast_height_of_term candidate_ty in
+ let rc = signature >= height in
+ if rc = false then
+ prerr_endline ("Filtro: " ^ NCicPp.ppterm ~context:[] ~subst:[]
+ ~metasenv:[] candidate ^ ": " ^ string_of_int height)
+ else
+ prerr_endline ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[]
+ ~metasenv:[] candidate ^ ": " ^ string_of_int height);
+
+ rc
+;;
let candidate_no = ref 0;;
let size = int "size" flags 10 in
let width = int "width" flags 4 (* (3+List.length goals)*) in
(* XXX fix sort *)
- let goals = List.map (fun i -> (i,P)) goals in
- let signature = () in
+(* let goals = List.map (fun i -> (i,P)) goals in *)
+ let signature = height_of_goals status in
let flags = {
last = true;
maxwidth = width;
ntheorem le_pred_n : ∀n:nat. pred n ≤ n.
#n; nelim n; //; nqed.
+(* XXX global problem *)
+nlemma my_trans_le : ∀x,y,z:nat.x ≤ y → y ≤ z → x ≤ z.
+napply transitive_le.
+nqed.
+
ntheorem monotonic_pred: monotonic ? le pred.
-#n; #m; #lenm; nelim lenm; //; /2/; nqed.
+#n; #m; #lenm; nelim lenm; /2/; nqed.
ntheorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
-/2/; nqed.
+(* XXX *) nletin hint ≝ monotonic. /2/; nqed.
-ntheorem lt_S_S_to_lt: ∀n,m. S n < S m \to n < m.
+ntheorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m.
/2/; nqed.
ntheorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
#n; #m; #lenm; nelim lenm; napplyS refl_eq. *)
napply nat_elim2;
##[//
- ##|#n; #abs; napply False_ind;/2/;
+ ##|#n; #abs; napply False_ind; (* XXX *) napply not_le_Sn_O; /2/.
##|#n; #m; #Hind; #c; napplyS Hind; /2/;
##]
nqed.
∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
napply nat_elim2;
##[//
- ##|#n; #p; #abs; napply False_ind;/2/;
+ ##|#n; #p; #abs; napply False_ind; (* XXX *) napply not_le_Sn_O; /2/;
##|nnormalize;/3/;
##]
nqed.
(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
napply nat_elim2;
##[#n; ncases n; nnormalize; /3/;
- ##|nnormalize; /3/;
- ##|nnormalize; /4/;
- ##]
+ ##|nnormalize; (* XXX *) nletin hint ≝ not_eq_O_S; /3/;
+ ##|nnormalize; /4/;
+ ##] (* XXX rimane aperto *) #m; #P; #_; #H; napply H; napply not_eq_O_S.
nqed.
ntheorem eqb_n_n: ∀n. eqb n n = true.
ntheorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
#n; #m; napply (eqb_elim n m);//;
-#_; #abs; napply False_ind;/2/;
+#_; #abs; napply False_ind; (* XXX *) nletin hint ≝ not_eq_true_false; /2/;
nqed.
ntheorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m.
(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
napply nat_elim2; nnormalize;
##[/2/
- ##|/3/;
+ ##| (* XXX *) nletin hint ≝ not_le_Sn_O; /3/;
##|#n; #m; #Hind; #P; #Pt; #Pf; napply Hind;
##[#lenm; napply Pt; napply le_S_S;//;
##|#nlenm; napply Pf; #leSS; /3/;
ntheorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m.
#n; #m; napply leb_elim;
##[//;
- ##|#_; #abs; napply False_ind; /2/;
+ ##|#_; #abs; napply False_ind; (* XXX *) nletin hint ≝ not_eq_true_false; /2/;
##]
nqed.
ntheorem leb_false_to_not_le:∀n,m.
leb n m = false → n ≰ m.
#n; #m; napply leb_elim;
- ##[#_; #abs; napply False_ind; /2/;
+ ##[#_; #abs; napply False_ind; (* XXX *) nletin hint ≝ not_eq_true_false; /2/;
##|/2/;
##]
nqed.
-overlap/o-algebra.ma sets/categories2.ma
algebra/bool.ma logic/connectives.ma
+overlap/o-algebra.ma sets/categories2.ma
algebra/abelian_magmas.ma algebra/magmas.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
+arithmetics/nat.ma basics/bool.ma basics/eq.ma basics/functions.ma hints_declaration.ma
logic/destruct_bb.ma logic/equality.ma
+datatypes/bool.ma logic/pts.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
+basics/bool.ma basics/eq.ma basics/functions.ma
topology/igft.ma logic/equality.ma sets/sets.ma
-nat/minus.ma nat/order.ma
+foo.ma logic/equality.ma logic/pts.ma nat/nat.ma
algebra/magmas.ma sets/sets.ma
+nat/minus.ma nat/order.ma
hints_declaration.ma logic/pts.ma
-Plogic/equality.ma logic/pts.ma
properties/relations1.ma logic/pts.ma
-algebra/unital_magmas.ma algebra/magmas.ma
-nat/compare.ma datatypes/bool.ma nat/order.ma
+Plogic/equality.ma logic/pts.ma
sets/categories.ma sets/sets.ma
properties/relations2.ma logic/pts.ma
+algebra/unital_magmas.ma algebra/magmas.ma
+nat/compare.ma datatypes/bool.ma nat/order.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
+basics/list.ma basics/bool.ma basics/eq.ma
sets/categories2.ma sets/categories.ma sets/setoids2.ma sets/sets.ma
+topology/igft-setoid.ma sets/sets.ma
sets/sets.ma hints_declaration.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
-datatypes/pairs.ma logic/pts.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
+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/big_ops.ma algebra/magmas.ma nat/order.ma
+topology/cantor.ma nat/nat.ma topology/igft.ma
sets/setoids2.ma properties/relations2.ma sets/setoids1.ma
+nat/big_ops.ma algebra/magmas.ma nat/order.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
+topology/igft3.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma
+topology/igft4.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma
basics/eq.ma basics/relations.ma
sets/setoids.ma hints_declaration.ma logic/connectives.ma properties/relations.ma
projects / helm.git / commitdiff