[Pkg-ocaml-maint-commits] [aac-tactics] 01/04: Imported Upstream version 0.4
Stéphane Glondu
glondu at moszumanska.debian.org
Fri Dec 6 07:50:32 UTC 2013
This is an automated email from the git hooks/post-receive script.
glondu pushed a commit to branch master
in repository aac-tactics.
commit a77bca84565b26aeedec3b210d761240d9d261f4
Author: Stephane Glondu <steph at glondu.net>
Date: Thu Dec 5 07:55:11 2013 +0100
Imported Upstream version 0.4
---
Caveats.v | 3 +
Makefile | 11 ++-
Tutorial.v | 33 +++++++++
aac.mlpack | 1 +
coq.ml | 2 +
coq.mli | 1 +
evm_compute.ml | 221 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
evm_compute.mli | 11 +++
rewrite.ml4 | 47 ++++++++++++
9 files changed, 327 insertions(+), 3 deletions(-)
diff --git a/Caveats.v b/Caveats.v
index a7967cc..d0ec37a 100644
--- a/Caveats.v
+++ b/Caveats.v
@@ -13,6 +13,7 @@
with the path to the [aac_tactics] library
*)
+Add Rec LoadPath "." as AAC_tactics.
Require Import AAC.
Require Instances.
@@ -370,3 +371,5 @@ to investigate on this in the future *)
End Z.
+
+
diff --git a/Makefile b/Makefile
index 1043ce9..03775bc 100644
--- a/Makefile
+++ b/Makefile
@@ -1,24 +1,29 @@
-FILES := coq.mli helper.mli search_monad.mli matcher.mli theory.mli print.mli rewrite.mli \
- coq.ml helper.ml search_monad.ml matcher.ml theory.ml print.ml rewrite.ml4 \
+FILES := coq.mli helper.mli search_monad.mli matcher.mli theory.mli print.mli \
+ evm_compute.mli evm_compute.ml \
+ coq.ml helper.ml search_monad.ml matcher.ml theory.ml print.ml rewrite.ml4 \
aac.mlpack \
AAC.v Instances.v Tutorial.v Caveats.v
ARGS := -R . AAC_tactics
-.PHONY: coq clean
+.PHONY: coq clean doc
world: all doc
all: Makefile.coq
$(MAKE) -f Makefile.coq all
+install: Makefile.coq
+ $(MAKE) -f Makefile.coq install
+
coq: Makefile.coq
$(MAKE) -f Makefile.coq
doc: Makefile.coq
$(MAKE) -f Makefile.coq html
+ $(MAKE) -f Makefile.coq mlihtml
Makefile.coq: Makefile $(VS)
coq_makefile $(ARGS) $(FILES) -o Makefile.coq
diff --git a/Tutorial.v b/Tutorial.v
index 76006ca..6356a10 100644
--- a/Tutorial.v
+++ b/Tutorial.v
@@ -397,3 +397,36 @@ Section Examples.
End Examples.
+Section Match.
+ (* The following example is inspired by a question by Francois
+ Pottier, wokring in the context of separation logic. *)
+
+ Variable T : Type.
+ Variable star : T -> T -> T.
+ Hypothesis P : T -> Prop.
+
+ Context (starA : Associative eq star).
+ Context (starC : Commutative eq star).
+
+ Hypothesis P_hereditary_left : forall a b, P (star a b) -> P a.
+ Hypothesis P_hereditary_right : forall a b, P (star a b) -> P b.
+
+ Notation "a * b" := (star a b).
+
+ Ltac crush :=
+ match goal with
+ H: P ?R' |- P ?R =>
+ let h := fresh in
+ aac_match (fun x => x * R) R' h;
+ rewrite <- h in H;
+ try eauto using P_hereditary_right
+ end.
+
+ Goal forall a b c, P (c * a * c * b) -> P (b * a).
+ Proof. intros. crush. Qed.
+
+ Goal forall a b c, exists d, P (d * a * c * b) -> P (b * d) /\ b = d.
+ Proof. intros. eexists. intros. split. crush. reflexivity. Qed.
+
+End Match.
+
diff --git a/aac.mlpack b/aac.mlpack
index 0c12567..60d5298 100644
--- a/aac.mlpack
+++ b/aac.mlpack
@@ -4,4 +4,5 @@ Search_monad
Matcher
Theory
Print
+Evm_compute
Rewrite
diff --git a/coq.ml b/coq.ml
index 7371913..132fbf7 100644
--- a/coq.ml
+++ b/coq.ml
@@ -148,6 +148,8 @@ module Leibniz = struct
let path = ["Coq"; "Init"; "Logic"]
let eq_refl = lazy (init_constant path "eq_refl")
let eq_refl ty x = lapp eq_refl [| ty;x|]
+ let eq ty = Term.mkApp (init_constant path "eq", [| ty |])
+
end
module Option = struct
diff --git a/coq.mli b/coq.mli
index a0f2ce0..53d42eb 100644
--- a/coq.mli
+++ b/coq.mli
@@ -79,6 +79,7 @@ end
module Leibniz : sig
val eq_refl : Term.types -> Term.constr -> Term.constr
+ val eq : Term.types -> Term.constr
end
module Option : sig
diff --git a/evm_compute.ml b/evm_compute.ml
new file mode 100644
index 0000000..b10a9cd
--- /dev/null
+++ b/evm_compute.ml
@@ -0,0 +1,221 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmp" i*)
+
+
+let pp_constr fmt x = Pp.pp_with fmt (Printer.pr_constr x)
+let pp_list pp fmt l = List.iter (fun x -> Format.fprintf fmt "%a; " pp x) l
+let pp_list_nl pp fmt l = List.iter (fun x -> Format.fprintf fmt "%a;\n" pp x) l
+let pp_constrs fmt l = (pp_list pp_constr) fmt l
+
+type constr = Term.constr
+
+module Replace (X : sig val eq: Term.constr -> Term.constr -> bool
+ val subst : (Term.constr * Term.constr) list end) =
+ struct
+
+ (* assumes that [c] and [t] have no outer casts, and all
+ applications have been flattened *)
+ let rec find l (t: constr) =
+ match l with
+ | [] -> None
+ | (c,c') :: q ->
+ begin
+ match Term.kind_of_term c, Term.kind_of_term t with
+ | Term.App (f1,args1), Term.App (f2, args2) ->
+ let l1 = Array.length args1 in
+ let l2 = Array.length args2 in
+ if l1 <= l2 && X.eq c (Term.mkApp (f2, Array.sub args2 0 l1))
+ then
+ (* we must return the array of arguments, to make the
+ substitution in them too *)
+ Some (c',Array.sub args2 l1 (l2 - l1))
+ else
+ find q t
+ | _, _ ->
+ if X.eq c t
+ then Some (c', [| |])
+ else find q t
+ end
+
+
+ let replace_terms t =
+ let rec aux (k:int) t =
+ match find X.subst t with
+ | Some (t',v) ->
+ let v' = Array.map (Term.map_constr_with_binders (succ) aux k) v in
+ Term.mkApp (Term.lift k t', v')
+ | None ->
+ Term.map_constr_with_binders succ aux k t
+ in aux 0 t
+
+ end
+
+let nowhere =
+ { Tacexpr.onhyps = Some [];
+ Tacexpr.concl_occs = Glob_term.no_occurrences_expr
+ }
+
+let mk_letin
+ (name:string)
+ (c: constr)
+ (k : Names .identifier -> Proof_type.tactic)
+: Proof_type.tactic =
+ fun goal ->
+ let name = (Names.id_of_string name) in
+ let name = Tactics.fresh_id [] name goal in
+ let letin = (Tactics.letin_tac None (Names.Name name) c None nowhere) in
+ Tacticals.tclTHEN letin (k name) goal
+
+let assert_tac
+ (name:string)
+ (c: constr)
+ (by:Proof_type.tactic)
+ (k : Names.identifier -> Proof_type.tactic)
+: Proof_type.tactic =
+ fun goal ->
+ let name = (Names.id_of_string name) in
+ let name = Tactics.fresh_id [] name goal in
+ let t = (Tactics.assert_tac (Names.Name name) c) in
+ Tacticals.tclTHENS t [by; (k name)] goal
+
+
+(* The contrib name is used to locate errors when loading constrs *)
+let contrib_name = "evm_compute"
+
+(* Getting constrs (primitive Coq terms) from existing Coq
+ libraries. *)
+let find_constant contrib dir s =
+ Libnames.constr_of_global (Coqlib.find_reference contrib dir s)
+
+let init_constant dir s = find_constant contrib_name dir s
+
+module Leibniz = struct
+ let path = ["Coq"; "Init"; "Logic"]
+
+ let eq_refl t x=
+ Term.mkApp (init_constant path "eq_refl", [| t; x|])
+
+ let eq t x y =
+ Term.mkApp (init_constant path "eq", [| t; x ; y|])
+
+ let eq_ind_r ty x p px y yx =
+ Term.mkApp (init_constant path "eq_ind_r", [|ty;x;p;px;y;yx|])
+end
+
+let mk_vm_cast t c = Term.mkCast (c,Term.VMcast,t)
+
+let mk_let
+ (name:Names.identifier)
+ (c: constr)
+ (t: constr)
+ (k : Names.identifier -> constr) =
+ Term.mkNamedLetIn name c t (Term.subst_vars [name] (k name))
+
+let mk_fun
+ (name:Names.identifier)
+ (t: constr)
+ (k : Names.identifier -> constr) =
+ Term.mkNamedLambda name t (Term.subst_vars [name] (k name))
+
+let rec has_evar x =
+ match Term.kind_of_term x with
+ | Term.Evar _ -> true
+ | Term.Rel _ | Term.Var _ | Term.Meta _ | Term.Sort _ | Term.Const _ | Term.Ind _ | Term.Construct _ ->
+ false
+ | Term.Cast (t1, _, t2) | Term.Prod (_, t1, t2) | Term.Lambda (_, t1, t2) ->
+ has_evar t1 || has_evar t2
+ | Term.LetIn (_, t1, t2, t3) ->
+ has_evar t1 || has_evar t2 || has_evar t3
+ | Term.App (t1, ts) ->
+ has_evar t1 || has_evar_array ts
+ | Term.Case (_, t1, t2, ts) ->
+ has_evar t1 || has_evar t2 || has_evar_array ts
+ | Term.Fix ((_, tr)) | Term.CoFix ((_, tr)) ->
+ has_evar_prec tr
+and has_evar_array x =
+ Util.array_exists has_evar x
+and has_evar_prec (_, ts1, ts2) =
+ Util.array_exists has_evar ts1 || Util.array_exists has_evar ts2
+
+let evm_compute eq blacklist = fun gl ->
+ (* the type of the conclusion of the goal is [concl] *)
+ let concl = Tacmach.pf_concl gl in
+
+ let extra =
+ List.fold_left (fun acc (id,body,ty) ->
+ match body with
+ | None -> acc
+ | Some body -> if has_evar body then (Term.mkVar id :: acc) else acc)
+ [] (Tacmach.pf_hyps gl) in
+
+ (* the set of evars that appear in the goal *)
+ let evars = Evd.evar_list (Tacmach.project gl) concl in
+
+ (* the arguments of the function are: the constr that are blacklisted, then the evars *)
+ let args = extra @ blacklist @ (List.map (fun x -> Term.mkEvar x) evars) in
+
+ let argsv = Array.of_list args in
+
+ let context = (Termops.rel_list 0 (List.length args)) in
+
+ (* we associate to each argument the proper de bruijn index *)
+ let (subst: (Term.constr * Term.constr) list) = List.combine args context in
+
+ let module R = Replace(struct let eq = eq let subst = subst end) in
+
+ let t = R.replace_terms concl in
+
+ (* we have to retype both the blacklist and the evars to know how to build the final product *)
+ let rel_context = List.map (fun x -> Names.Anonymous, None, Tacmach.pf_type_of gl x) args in
+
+ (* the abstraction *)
+ let t = Term.it_mkLambda_or_LetIn t (List.rev rel_context) in
+
+ let typeof_t = (Tacmach.pf_type_of gl t) in
+
+ (* the normal form of the head function *)
+ let nft = Vnorm.cbv_vm (Tacmach.pf_env gl) t typeof_t in
+
+
+ let (!!) x = Tactics.fresh_id [] ((Names.id_of_string x)) gl in
+
+ (* p = [fun x => x a_i] which corresponds to the type of the goal when applied to [t] *)
+ let p = mk_fun (!! "x") typeof_t (fun x -> Term.mkApp (Term.mkVar x,argsv)) in
+
+ let proof_term pnft = begin
+ mk_let (!! "nft") nft typeof_t (fun nft -> let nft' = Term.mkVar nft in
+ mk_let (!! "t") t typeof_t (fun t -> let t' = Term.mkVar t in
+ mk_let (!! "H") (mk_vm_cast (Leibniz.eq typeof_t t' nft') (Leibniz.eq_refl typeof_t nft')) (Leibniz.eq typeof_t t' nft')
+ (fun h ->
+ (* typeof_t -> Prop *)
+ let body = Leibniz.eq_ind_r typeof_t
+ nft' p pnft t' (Term.mkVar h)
+ in
+ Term.mkCast (body, Term.DEFAULTcast, Term.mkApp (t', argsv))
+ )))
+ end in
+
+ try
+ assert_tac "subgoal" (Term.mkApp (p,[| nft |]))
+ Tacticals.tclIDTAC
+ (fun subgoal ->
+ (* We use the tactic [exact_no_check]. It has two consequences:
+ - first, it means that in theory we could produce ill typed proof terms, that fail to type check at Qed;
+ - second, it means that we are able to use vm_compute and vm_compute casts, that will be checkable at Qed time when all evars have been instantiated.
+ *)
+ Tactics.exact_no_check (proof_term (Term.mkVar subgoal))
+ ) gl
+ with
+ | e ->
+ Tacticals.tclFAIL 0 (Pp.str (Printf.sprintf "evm_compute failed with an exception %s" (Printexc.to_string e))) gl
+
+;;
+
+let evm_compute_in eq blacklist h = fun gl ->
+ let concl = Tacmach.pf_concl gl in
+ Tacticals.tclTHENLIST
+ [Tactics.revert [h];
+ evm_compute eq (concl :: blacklist);
+ Tactics.introduction h
+ ]
+ gl
diff --git a/evm_compute.mli b/evm_compute.mli
new file mode 100644
index 0000000..f50c0db
--- /dev/null
+++ b/evm_compute.mli
@@ -0,0 +1,11 @@
+
+
+(** [evm_compute eq blacklist] performs a vm_compute step with the
+ following provisos: evars can appear in the goal; terms that are
+ equal (modulo eq) to terms in the blacklist are abstracted
+ before-hand. *)
+val evm_compute : (Term.constr -> Term.constr -> bool) -> Term.constr list -> Proof_type.tactic
+
+
+(** [evm_compute eq blacklist h] performs an evm_compute step in the hypothesis h *)
+val evm_compute_in : (Term.constr -> Term.constr -> bool) -> Term.constr list -> Names.identifier -> Proof_type.tactic
diff --git a/rewrite.ml4 b/rewrite.ml4
index 6229262..383d706 100644
--- a/rewrite.ml4
+++ b/rewrite.ml4
@@ -32,6 +32,10 @@ let push_anomaly msg = function
| Util.Anomaly _ as e -> raise e
| _ -> Coq.anomaly msg
+
+
+
+
module M = Matcher
open Term
@@ -435,6 +439,41 @@ let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict
) goal
+(** [aac_match eq (fun x1 ... xn => p) t H] match the term [t] against
+ the pattern, and introduces an hypothesis H of type p = t. (Note
+ that we have performed the substitution in p).
+*)
+
+let aac_match ~eq pattern term h = fun gl ->
+ let env = Tacmach.pf_env gl in
+ let evar_map = Tacmach.project gl in
+ let carrier = Typing.type_of env evar_map term in
+ let rel = Coq.Relation.make carrier eq in
+ let equiv,gl = Coq.Equivalence.from_relation gl rel in
+ (* first, we decompose the pattern as an arity. *)
+ let x_args, pat = Term.decompose_lam pattern in
+ (* then, we reify the pattern and the term, using the provided equality *)
+ let envs = Theory.Trans.empty_envs () in
+ let left, right,gl = Theory.Trans.t_of_constr gl rel envs (pat,term) in
+ let gl,ir = Theory.Trans.ir_of_envs gl rel envs in
+ let solutions = Matcher.matcher (Theory.Trans.ir_to_units ir) left right in
+ (* then, we pick the first solution to the matching problem *)
+ let sigma = match Search_monad.choose solutions with
+ | None -> Coq.user_error "no solution to the matching problem"
+ | Some sigma -> sigma
+ in
+ let p_sigma = Matcher.Subst.instantiate sigma left in
+ let args = List.map (fun (x,t) -> x,Theory.Trans.raw_constr_of_t ir rel [] t) (Matcher.Subst.to_list sigma) in
+ (* Then, we have to assert the fact that p_sigma is equal to term *)
+ let equation = mkApp (eq, [| Theory.Trans.raw_constr_of_t ir rel [] p_sigma ; term |]) in
+ let evar_map = Tacmach.project gl in
+ Tacticals.tclTHENLIST
+ [
+ Refiner.tclEVARS evar_map;
+ Tactics.assert_by h equation (by_aac_reflexivity term equiv ir p_sigma right);
+ ] gl
+
+
open Coq.Rewrite
open Tacmach
open Tacticals
@@ -522,3 +561,11 @@ TACTIC EXTEND _aacu_instances_
| [ "aacu_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
[ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl ]
END
+
+TACTIC EXTEND _aac_match_
+| [ "aac_match" constr(p) constr(t) ident(h)] ->
+ [ fun gl ->
+ let ty = Tacmach.pf_type_of gl t in
+ let eq = Coq.Leibniz.eq ty in
+ aac_match ~eq p t (Names.Name h) gl]
+END
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/aac-tactics.git
More information about the Pkg-ocaml-maint-commits
mailing list