*)
module C = Cic
+module I = CicInspect
module D = Deannotate
module DTI = DoubleTypeInference
module TC = CicTypeChecker
let decurry = List.length classes - List.length tl in
if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
- let synth = Cl.S.singleton 0 in
+ let synth = I.S.singleton 0 in
let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
match rc with
| Some (i, j) when i > 1 && i <= List.length classes ->
let classes, tl, _, what = split2_last classes tl in
let script, what = mk_atomic st dtext what in
- let synth = Cl.S.add 1 synth in
+ let synth = I.S.add 1 synth in
let qs = mk_bkd_proofs (next st) synth classes tl in
if is_rewrite_right hd then
List.rev script @ convert st t @
try
let _, dtext = test_depth st in
let aux inv v =
- if Cl.overlaps synth inv then None else
- if Cl.S.is_empty inv then Some (mk_proof st v) else
+ if I.overlaps synth inv then None else
+ if I.S.is_empty inv then Some (mk_proof st v) else
Some [T.Apply (v, dtext ^ "dependent")]
in
T.list_map2_filter aux classes ts
module C = Cic
module R = CicReduction
module D = Deannotate
-module Int = struct
- type t = int
- let compare = compare
-end
-module S = Set.Make (Int)
+module I = CicInspect
type conclusion = (int * int) option
(* debugging ****************************************************************)
let string_of_entry inverse =
- if S.mem 0 inverse then "C" else
- if S.is_empty inverse then "I" else "P"
+ if I.S.mem 0 inverse then "C" else
+ if I.S.is_empty inverse then "I" else "P"
let to_string (classes, rc) =
let linearize = String.concat " " (List.map string_of_entry classes) in
let out_table b =
let map i (_, inverse) =
let map i tl = Printf.sprintf "%2u" i :: tl in
- let iset = String.concat " " (S.fold map inverse []) in
+ let iset = String.concat " " (I.S.fold map inverse []) in
Printf.eprintf "%2u|%s\n" i iset
in
Array.iteri map b;
let id x = x
-let rec list_fold_left g map = function
- | [] -> g
- | hd :: tl -> map (list_fold_left g map tl) hd
-
-let get_rels h t =
- let rec aux d g = function
- | C.Sort _
- | C.Implicit _ -> g
- | C.Rel i ->
- if i < d then g else fun a -> g (S.add (i - d + h + 1) a)
- | C.Appl ss -> list_fold_left g (aux d) ss
- | C.Const (_, ss)
- | C.MutInd (_, _, ss)
- | C.MutConstruct (_, _, _, ss)
- | C.Var (_, ss) ->
- let map g (_, t) = aux d g t in
- list_fold_left g map ss
- | C.Meta (_, ss) ->
- let map g = function
- | None -> g
- | Some t -> aux d g t
- in
- list_fold_left g map ss
- | C.Cast (t1, t2) -> aux d (aux d g t2) t1
- | C.LetIn (_, t1, t2)
- | C.Lambda (_, t1, t2)
- | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
- | C.MutCase (_, _, t1, t2, ss) ->
- aux d (aux d (list_fold_left g (aux d) ss) t2) t1
- | C.Fix (_, ss) ->
- let k = List.length ss in
- let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in
- list_fold_left g map ss
- | C.CoFix (_, ss) ->
- let k = List.length ss in
- let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in
- list_fold_left g map ss
- in
- let g a = a in
- aux 1 g t S.empty
-
let split c t =
let add s v c = Some (s, C.Decl v) :: c in
let rec aux whd a n c = function
try
let vs, h = split c t in
let rc = classify_conclusion (List.hd vs) in
- let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in
+ let map (b, h) v = (I.get_rels_from_premise h v, I.S.empty) :: b, succ h in
let l, h = List.fold_left map ([], 0) vs in
let b = Array.of_list (List.rev l) in
let mk_closure b h =
- let map j = if j < h then S.union (fst b.(j)) else id in
+ let map j = if j < h then I.S.union (fst b.(j)) else id in
for i = pred h downto 0 do
let direct, unused = b.(i) in
- b.(i) <- S.fold map direct direct, unused
+ b.(i) <- I.S.fold map direct direct, unused
done; b
in
let b = mk_closure b h in
let rec mk_inverse i direct =
- if S.is_empty direct then () else
- let j = S.choose direct in
+ if I.S.is_empty direct then () else
+ let j = I.S.choose direct in
if j < h then
let unused, inverse = b.(j) in
- b.(j) <- unused, S.add i inverse
+ b.(j) <- unused, I.S.add i inverse
else ();
- mk_inverse i (S.remove j direct)
+ mk_inverse i (I.S.remove j direct)
in
let map i (direct, _) = mk_inverse i direct in
Array.iteri map b;
(* out_table b; *)
List.rev_map snd (List.tl (Array.to_list b)), rc
with Invalid_argument _ -> failwith "Classify.classify"
-
-let overlaps s1 s2 =
- let predicate x = S.mem x s1 in
- S.exists predicate s2
* http://cs.unibo.it/helm/.
*)
-module S : Set.S with type elt = int
-
type conclusion = (int * int) option
-val classify: Cic.context -> Cic.term -> S.t list * conclusion
-
-val to_string: S.t list * conclusion -> string
+val classify: Cic.context -> Cic.term -> CicInspect.S.t list * conclusion
-val overlaps: S.t -> S.t -> bool
+val to_string: CicInspect.S.t list * conclusion -> string
val split: Cic.context -> Cic.term -> Cic.term list * int
discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi
path_indexing.cmo: cic.cmo path_indexing.cmi
path_indexing.cmx: cic.cmx path_indexing.cmi
+cicInspect.cmo: cic.cmo cicInspect.cmi
+cicInspect.cmx: cic.cmx cicInspect.cmi
discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi
path_indexing.cmo: cic.cmx path_indexing.cmi
path_indexing.cmx: cic.cmx path_indexing.cmi
+cicInspect.cmo: cic.cmx cicInspect.cmi
+cicInspect.cmx: cic.cmx cicInspect.cmi
cicParser.mli \
cicUtil.mli \
helmLibraryObjects.mli \
- libraryObjects.mli \
+ libraryObjects.mli \
discrimination_tree.mli \
- path_indexing.mli
+ path_indexing.mli \
+ cicInspect.mli
IMPLEMENTATION_FILES = \
cic.ml $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi
--- /dev/null
+(* Copyright (C) 2003-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module UM = UriManager
+module C = Cic
+
+module Int = struct
+ type t = int
+ let compare = compare
+end
+module S = Set.Make (Int)
+
+let overlaps s1 s2 =
+ let predicate x = S.mem x s1 in
+ S.exists predicate s2
+
+let get_rels_from_premise h t =
+ let rec aux d g = function
+ | C.Sort _
+ | C.Implicit _ -> g
+ | C.Rel i ->
+ if i < d then g else fun a -> g (S.add (i - d + h + 1) a)
+ | C.Appl ss -> List.fold_left (aux d) g ss
+ | C.Const (_, ss)
+ | C.MutInd (_, _, ss)
+ | C.MutConstruct (_, _, _, ss)
+ | C.Var (_, ss) ->
+ let map g (_, t) = aux d g t in
+ List.fold_left map g ss
+ | C.Meta (_, ss) ->
+ let map g = function
+ | None -> g
+ | Some t -> aux d g t
+ in
+ List.fold_left map g ss
+ | C.Cast (t1, t2) -> aux d (aux d g t2) t1
+ | C.LetIn (_, t1, t2)
+ | C.Lambda (_, t1, t2)
+ | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
+ | C.MutCase (_, _, t1, t2, ss) ->
+ aux d (aux d (List.fold_left (aux d) g ss) t2) t1
+ | C.Fix (_, ss) ->
+ let k = List.length ss in
+ let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in
+ List.fold_left map g ss
+ | C.CoFix (_, ss) ->
+ let k = List.length ss in
+ let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in
+ List.fold_left map g ss
+ in
+ let g a = a in
+ aux 1 g t S.empty
+
+let get_mutinds_of_uri u t =
+ let rec aux g = function
+ | C.Sort _
+ | C.Implicit _
+ | C.Rel _ -> g
+ | C.Appl ss -> List.fold_left aux g ss
+ | C.Const (_, ss)
+ | C.MutConstruct (_, _, _, ss)
+ | C.Var (_, ss) ->
+ let map g (_, t) = aux g t in
+ List.fold_left map g ss
+ | C.MutInd (uri, tyno, ss) ->
+ let map g (_, t) = aux g t in
+ let g = List.fold_left map g ss in
+ if UM.eq u uri then fun a -> g (S.add tyno a) else g
+ | C.Meta (_, ss) ->
+ let map g = function
+ | None -> g
+ | Some t -> aux g t
+ in
+ List.fold_left map g ss
+ | C.Cast (t1, t2) -> aux (aux g t2) t1
+ | C.LetIn (_, t1, t2)
+ | C.Lambda (_, t1, t2)
+ | C.Prod (_, t1, t2) -> aux (aux g t2) t1
+ | C.MutCase (_, _, t1, t2, ss) ->
+ aux (aux (List.fold_left aux g ss) t2) t1
+ | C.Fix (_, ss) ->
+ let map g (_, _, t1, t2) = aux (aux g t2) t1 in
+ List.fold_left map g ss
+ | C.CoFix (_, ss) ->
+ let map g (_, t1, t2) = aux (aux g t2) t1 in
+ List.fold_left map g ss
+ in
+ let g a = a in
+ aux g t S.empty
--- /dev/null
+(* Copyright (C) 2003-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module S: Set.S with type elt = int
+
+val overlaps: S.t -> S.t -> bool
+
+val get_rels_from_premise: int -> Cic.term -> S.t
+
+val get_mutinds_of_uri: UriManager.uri -> Cic.term -> S.t
(* $Id$ *)
module C = Cic
+module I = CicInspect
+module S = CicSubstitution
+module TC = CicTypeChecker
module P = PrimitiveTactics
module T = Tacticals
-module S = ProofEngineStructuralRules
+module PESR = ProofEngineStructuralRules
module F = FreshNamesGenerator
module PET = ProofEngineTypes
module H = ProofEngineHelpers
let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None
-let get_inductive_type uri tyno =
+let get_inductive_def uri =
match E.get_obj Un.empty_ugraph uri with
| C.InductiveDefinition (tys, _, lpsno, _), _ ->
- let _, inductive, arity, _ = List.nth tys tyno in
- lpsno, inductive, arity
+ lpsno, tys
| _ -> assert false
-let rec check_type = function
- | C.MutInd (uri, tyno, _) ->
- let lpsno, inductive, arity = get_inductive_type uri tyno in
+let is_not_recursive uri tyno tys =
+ let map mutinds (_, ty) =
+(* FG: we can do much better here *)
+ let map mutinds t = I.S.union mutinds (I.get_mutinds_of_uri uri t) in
+(**********************************)
+ let premises, _ = split [] ty in
+ List.fold_left map mutinds (List.tl premises)
+ in
+ let _, _, _, constructors = List.nth tys tyno in
+ let mutinds = List.fold_left map I.S.empty constructors in
+ I.S.is_empty mutinds
+
+let rec check_type sorts metasenv context = function
+ | C.MutInd (uri, tyno, _) as t ->
+ let lpsno, tys = get_inductive_def uri in
+ let _, inductive, arity, _ = List.nth tys tyno in
let _, psno = split [] arity in
- if lpsno <> psno && inductive then Other else Ind
+ let not_relation = (lpsno = psno) in
+ let not_recursive = is_not_recursive uri tyno tys in
+ let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in
+ let sort = match split context ty_ty with
+ | C.Sort sort ::_ , _ -> CicPp.ppsort sort
+ | C.Meta _ :: _, _ -> CicPp.ppsort (C.Type (Un.fresh ()))
+ | _ -> assert false
+ in
+ let right_sort = List.mem sort sorts in
+ if not_relation && inductive && not_recursive && right_sort then
+ (HLog.warn (Printf.sprintf "Decomposing %s %u %b %u %u %b" (UriManager.string_of_uri uri) (succ tyno) inductive lpsno psno not_recursive);
+ Ind)
+ else Other
(* | C.Const (uri, _) as t ->
if List.mem (uri, None) types then Con (PET.const_lazy_term t) else Other
-*) | C.Appl (hd :: tl) -> check_type hd
+*) | C.Appl (hd :: tl) -> check_type sorts metasenv context hd
| _ -> Other
(* unexported tactics *******************************************************)
in
PET.mk_tactic scan_tac
-let elim_clear_unfold_tac ~mk_fresh_name_callback ~what =
+let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
let elim_clear_unfold_tac status =
let (proof, goal) = status in
let _, metasenv, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let index, ty = H.lookup_type metasenv context what in
- let tac = match check_type ty with
+ let tac = match check_type sorts metasenv context (S.lift index ty) with
| Ind -> T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
- ~continuation:(S.clear [what])
+ ~continuation:(PESR.clear [what])
| Con t -> RT.unfold_tac (Some t) ~pattern:(premise_pattern what)
| Other ->
let msg = "unexported elim_clear: not an decomposable type" in
(* roba seria ------------------------------------------------------------- *)
-let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
+let decompose_tac ?(sorts=[CicPp.ppsort C.Prop])
+ ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
let decompose_tac status =
let (proof, goal) = status in
let _, metasenv,_,_, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
- let tactic = elim_clear_unfold_tac ~mk_fresh_name_callback in
+ let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
let old_context_length = List.length context in
let tac = scan_tac ~old_context_length ~index:old_context_length ~tactic
in
?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
val decompose_tac:
+ ?sorts:string list ->
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
unit -> ProofEngineTypes.tactic
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Feb 21 14:36:23 CET 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Sun Feb 25 17:03:54 CET 2007 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
Cic.term -> ProofEngineTypes.tactic
val decompose :
+ ?sorts:string list ->
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
unit -> ProofEngineTypes.tactic
val demodulate :
include "NPlus/defs.ma".
-inductive NLE (q:Nat) (r:Nat): Prop \def
- | nle_nplus: \forall p. (p + q == r) \to NLE q r.
+inductive NLE: Nat \to Nat \to Prop \def
+ | nle_zero_1: \forall q. NLE zero q
+ | nle_succ_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q)
+.
(*CSC: the URI must disappear: there is a bug now *)
interpretation "natural 'greater or equal to'" 'geq y x=
set "baseuri" "cic:/matita/RELATIONAL/NLE/inv".
-include "NPlus/inv.ma".
include "NLE/defs.ma".
theorem nle_inv_succ_1: \forall x,y. x < y \to
\exists z. y = succ z \land x <= z.
- intros. elim H.
- lapply linear nplus_inv_succ_2 to H1.
- decompose. subst. auto depth = 4.
+ intros. inversion H; clear H; intros; subst;
+ [ destruct H
+ | destruct H2. clear H2. subst. auto
+ ]
qed.
theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y.
- intros.
- lapply linear nle_inv_succ_1 to H. decompose.
- destruct H1. clear H1. subst.
- auto.
+ intros. inversion H; clear H; intros; subst;
+ [ destruct H
+ | destruct H2. destruct H3. clear H2 H3. subst. auto
+ ]
qed.
theorem nle_inv_succ_zero: \forall x. x < zero \to False.
- intros.
- lapply linear nle_inv_succ_1 to H. decompose.
- destruct H1.
+ intros. inversion H; clear H; intros; subst;
+ [ destruct H
+ | destruct H3
+ ]
qed.
theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero.
- intros 1. elim x; clear x; intros;
+ intros. inversion H; clear H; intros; subst;
[ auto
- | lapply linear nle_inv_succ_zero to H1. decompose.
+ | destruct H3
].
qed.
theorem nle_inv_succ_2: \forall y,x. x <= succ y \to
x = zero \lor \exists z. x = succ z \land z <= y.
- intros 2; elim x; clear x; intros;
+ intros. inversion H; clear H; intros; subst;
[ auto
- | lapply linear nle_inv_succ_succ to H1.
- auto depth = 4.
+ | destruct H3. clear H3. subst. auto depth = 4
].
qed.
include "NLE/defs.ma".
+theorem nle_nplus: \forall p, q, r. (p + q == r) \to q <= r.
+ intros. elim H; clear H q r; auto.
+qed.
+
axiom nle_nplus_comp: \forall x1, x2, x3. (x1 + x2 == x3) \to
\forall y1, y2, y3. (y1 + y2 == y3) \to
x1 <= y1 \to x2 <= y2 \to x3 <= y3.
set "baseuri" "cic:/matita/RELATIONAL/NLE/props".
-include "NLE/inv.ma".
-
-theorem nle_zero_1: \forall q. zero <= q.
- intros. auto.
-qed.
-
-theorem nle_succ_succ: \forall p,q. p <= q \to succ p <= succ q.
- intros. elim H. clear H. auto.
-qed.
-
-theorem nle_ind: \forall P:(Nat \to Nat \to Prop).
- (\forall n:Nat.P zero n) \to
- (\forall n,n1:Nat.
- n <= n1 \to P n n1 \to P (succ n) (succ n1)
- ) \to
- \forall n,n1:Nat. n <= n1 \to P n n1.
- intros 4. elim n; clear n;
- [ auto
- | lapply linear nle_inv_succ_1 to H3. decompose; subst.
- auto
- ].
-qed.
-
-theorem nle_refl: \forall x. x <= x.
- intros 1; elim x; clear x; intros; auto.
-qed.
+include "NLE/order.ma".
theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y.
- intros. elim H using nle_ind; clear H x y; auto.
-qed.
-
-theorem nle_false: \forall x,y. x <= y \to y < x \to False.
- intros 3; elim H using nle_ind; clear H x y; auto.
-qed.
-
-theorem nle_trans: \forall x,y. x <= y \to
- \forall z. y <= z \to x <= z.
- intros 3. elim H using nle_ind; clear H x y;
- [ auto
- | lapply linear nle_inv_succ_1 to H3. decompose. subst.
- auto
- ].
-qed.
-
-theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y.
- intros. elim H using nle_ind; clear H x y;
- [ elim n; clear n; auto
- | decompose; subst; auto
- ].
+ intros. elim H; clear H x y; auto.
qed.
-theorem nle_gt_or_le: \forall x,y. y > x \lor y <= x.
+theorem nle_gt_or_le: \forall x, y. y > x \lor y <= x.
intros 2; elim y; clear y;
[ auto
| decompose;
- [ lapply linear nle_inv_succ_1 to H1. decompose.
- subst. auto depth=4
- | lapply linear nle_lt_or_eq to H1; decompose;
- subst; auto
- ]
+ [ lapply linear nle_inv_succ_1 to H1
+ | lapply linear nle_lt_or_eq to H1
+ ]; decompose; subst; auto depth = 4
].
qed.
For each each premise <command>H</command>
of type <command>T</command> in the current context
where <command>T</command> is a non-recursive inductive type
- withour right parameters, the tactic runs
+ of sort Prop without right parameters, the tactic runs
<command>
elim H as H<subscript>1</subscript> ... H<subscript>m</subscript>
</command>, clears <command>H</command> and runs itself
projects / helm.git / commitdiff