- proceduralClassify type argument are no longer critical: let's see how it goes
- acic2Procedural: the inline parameter Debug now works
- procedural2: we remove the conversions before first order relexivities (exp. to avoid conversion to []=[] in list/list.ma [does not work because []=[] in an open term since the equality type is unspecified]). so we we strengthen reflexivity (see below)
- setoids: now reflexivity is retried after whd if it fails in the first place.
- grafiteAst: detection of convertible rewrites is now optional and activated with the inline parameter "cr". nat/factorial2 is very slow without rewrites
transcript: we now avoid the generation of dupplicated inlines (mistakely generated by the grafite parser [this can not be avoided without a better syntax for .ma scripts])
now list/list.ma is fully reconstructed :)
nat/factorial2.ma takes long to be produced 22m31. Some conversion is slowing the process. nat/bertrand.ma also: we are waiting for it now :(
let rec is_debug n = function
| [] -> false
- | G.IPDebug debug :: _ -> debug <= n
+ | G.IPDebug debug :: _ -> n <= debug
| _ :: tl -> is_debug n tl
max_depth: int option;
depth : int;
defaults : bool;
+ cr : bool;
context : C.context;
case : int list
}
let get_type msg st t = H.get_type msg st.context (H.cic t)
let get_uri_of_head = function
- | C.AConst (_, u, _)
- | C.AAppl (_, C.AConst (_, u, _) :: _) -> Some (u, 0, 0)
- | C.AMutInd (_, u, i, _)
- | C.AAppl (_, C.AMutInd (_, u, i, _) :: _) -> Some (u, succ i, 0)
- | C.AMutConstruct (_, u, i, j, _)
- | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: _) -> Some (u, succ i, j)
- | _ -> None
+ | C.AConst (_, u, _) ->
+ Some (u, 0, 0, 0)
+ | C.AAppl (_, C.AConst (_, u, _) :: vs) ->
+ Some (u, 0, 0, List.length vs)
+ | C.AMutInd (_, u, i, _) ->
+ Some (u, succ i, 0, 0)
+ | C.AAppl (_, C.AMutInd (_, u, i, _) :: vs) ->
+ Some (u, succ i, 0, List.length vs)
+ | C.AMutConstruct (_, u, i, j, _) ->
+ Some (u, succ i, j, 0)
+ | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: vs) ->
+ Some (u, succ i, j, List.length vs)
+ | _ ->
+ None
let get_uri_of_apply = function
| T.Exact (t, _)
let is_reflexivity st step =
match get_uri_of_apply step with
- | None -> false
- | Some (uri, i, j) -> st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1
+ | None -> false
+ | Some (uri, i, j, n) ->
+ st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1 && n = 0
+
+let is_ho_reflexivity st step =
+ match get_uri_of_apply step with
+ | None -> false
+ | Some (uri, i, j, n) ->
+ st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1 && n > 0
let are_convertible st pred sx dx =
let pred, sx, dx = H.cic pred, H.cic sx, H.cic dx in
let mk_preamble st what script = match script with
| step :: script when is_reflexivity st step ->
+ T.Reflexivity (T.note_of_step step) :: script
+ | step :: script when is_ho_reflexivity st step ->
convert st what @ T.Reflexivity (T.note_of_step step) :: script
| T.Exact _ :: _ -> script
| _ -> convert st what @ script
let e = Cn.mk_pattern 1 ity pred in
let script = [T.Branch (qs, "")] in
if Cn.does_not_occur e then script else
- if are_convertible st pred sx dx then
+ if st.cr && are_convertible st pred sx dx then
let dtext = "convertible rewrite" ^ dtext in
let ity, ety, e = Cn.beta sx pred, Cn.beta dx pred, Cn.hole "" in
let city, cety = H.cic ity, H.cic ety in
max_depth = List.fold_left depth_map None params;
depth = 0;
defaults = not (List.mem G.IPNoDefaults params);
+ cr = List.mem G.IPCR params;
context = context;
case = []
}
let rc = classify_conclusion vs in
let map (b, h) (c, v) =
let _, argsno = PEH.split_with_whd (c, v) in
- let isf = argsno > 0 || H.is_sort v in
+ let isf = argsno > 0 (* || H.is_sort v *) in
let iu = H.is_unsafe h (List.hd vs) in
(I.get_rels_from_premise h v, I.S.empty, isf && iu) :: b, succ h
in
let set_items st name items =
let i = get_index st name in
let script = st.scripts.(i) in
- let contents = List.rev_append items script.contents in
+ let contents = List.rev_append (X.list_uniq items) script.contents in
st.scripts.(i) <- {script with name = name; contents = contents}
let set_heading st name =
type inline_param = IPPrefix of string (* undocumented *)
| IPAs of Cic.object_flavour (* preferred flavour *)
+ | IPCoercions (* show coercions *)
+ | IPDebug of int (* set debug level *)
| IPProcedural (* procedural rendering *)
| IPNoDefaults (* no default-based tactics *)
| IPLevel of int (* granularity level *)
| IPDepth of int (* undocumented *)
| IPComments (* show statistics *)
- | IPCoercions (* show coercions *)
- | IPDebug of int (* set debug level *)
+ | IPCR (* detect convertible rewriting *)
type ('term,'lazy_term) macro =
(* Whelp's stuff *)
let pp_param = function
| IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\""
| IPAs flavour -> flavour_pp flavour
+ | IPCoercions -> "coercions"
+ | IPDebug debug -> "debug = " ^ string_of_int debug
| IPProcedural -> "procedural"
| IPNoDefaults -> "nodefaults"
| IPDepth depth -> "depth = " ^ string_of_int depth
| IPLevel level -> "level = " ^ string_of_int level
| IPComments -> "comments"
- | IPCoercions -> "coercions"
- | IPDebug debug -> "debug = " ^ string_of_int debug
+ | IPCR -> "cr"
in
let s = String.concat " " (List.map pp_param l) in
if s = "" then s else " " ^ s
[ params = LIST0
[ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
| flavour = inline_flavour -> G.IPAs flavour
+ | IDENT "coercions" -> G.IPCoercions
+ | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
| IDENT "procedural" -> G.IPProcedural
| IDENT "nodefaults" -> G.IPNoDefaults
| IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
| IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
| IDENT "comments" -> G.IPComments
- | IDENT "coercions" -> G.IPCoercions
- | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
+ | IDENT "cr" -> G.IPCR
] -> params
]
];
primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi
ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \
primitiveTactics.cmx equalityTactics.cmx eliminationTactics.cmx ring.cmi
-setoids.cmo: proofEngineTypes.cmi primitiveTactics.cmi equalityTactics.cmi \
- setoids.cmi
-setoids.cmx: proofEngineTypes.cmx primitiveTactics.cmx equalityTactics.cmx \
- setoids.cmi
+setoids.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
+ primitiveTactics.cmi equalityTactics.cmi setoids.cmi
+setoids.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
+ primitiveTactics.cmx equalityTactics.cmx setoids.cmi
fourier.cmo: fourier.cmi
fourier.cmx: fourier.cmi
fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \
primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi
ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \
primitiveTactics.cmx equalityTactics.cmx eliminationTactics.cmx ring.cmi
-setoids.cmo: proofEngineTypes.cmi primitiveTactics.cmi equalityTactics.cmi \
- setoids.cmi
-setoids.cmx: proofEngineTypes.cmx primitiveTactics.cmx equalityTactics.cmx \
- setoids.cmi
+setoids.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
+ primitiveTactics.cmi equalityTactics.cmi setoids.cmi
+setoids.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
+ primitiveTactics.cmx equalityTactics.cmx setoids.cmi
fourier.cmo: fourier.cmi
fourier.cmx: fourier.cmi
fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \
(* $Id: setoid_replace.ml 8900 2006-06-06 14:40:27Z letouzey $ *)
+module T = Tacticals
+module RT = ReductionTactics
+module PET = ProofEngineTypes
+
let default_eq () =
match LibraryObjects.eq_URI () with
Some uri -> uri
in
ProofEngineTypes.mk_tactic tac
+let setoid_reflexivity_tac =
+ let start_tac = RT.whd_tac ~pattern:(PET.conclusion_pattern None) in
+ let fail_tac = T.then_ ~start:start_tac ~continuation:setoid_reflexivity_tac in
+ T.if_ ~start:setoid_reflexivity_tac ~continuation:T.id_tac ~fail:fail_tac
+
let setoid_symmetry =
let tac status =
try
| step : \forall l1,l2:list A. \forall x,y:A.
permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).
-include "nat/nat.ma".
-
+(*
+
definition x1 \def S O.
definition x2 \def S x1.
definition x3 \def S x2.
apply (step ? (x1::[]) [] x2 x3).
qed.
-
-(*
theorem nil_append_nil_both:
\forall A:Type.\forall l1,l2:list A.
l1 @ l2 = [] \to l1 = [] \land l2 = [].
-*)
-
-(*
-include "nat/nat.ma".
theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: [].
reflexivity.
simplify.
reflexivity.
qed.
+
*)
definition nth ≝
projects / helm.git / commitdiff