Permalink
Browse files

Add lets to the blacklist

That is, handle goals where hyps have bodies that contain evars
  • Loading branch information...
1 parent 179ba11 commit 2ef1dc51b40f428b46c7b927ff46f30579a932fb @braibant committed Jan 24, 2013
Showing with 69 additions and 10 deletions.
  1. +37 −9 src/evm_compute.ml4
  2. +32 −1 test-suite/Example.v
View
@@ -101,30 +101,55 @@ end
let mk_vm_cast t c = Term.mkCast (c,Term.VMcast,t)
let mk_let
- (name:string)
+ (name:Names.identifier)
(c: constr)
(t: constr)
(k : Names.identifier -> constr) =
- let name = (Names.id_of_string name) in
Term.mkNamedLetIn name c t (Term.subst_vars [name] (k name))
let mk_fun
- (name:string)
+ (name:Names.identifier)
(t: constr)
(k : Names.identifier -> constr) =
- let name = (Names.id_of_string name) in
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 = blacklist @ (List.map (fun x -> Term.mkEvar x) evars) in
+ let args = extra @ blacklist @ (List.map (fun x -> Term.mkEvar x) evars) in
let argsv = Array.of_list args in
@@ -148,13 +173,16 @@ let evm_compute eq blacklist = fun gl ->
(* 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 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')
+ 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
View
@@ -68,6 +68,22 @@ Time cbv; reflexivity.
Time Qed.
+(* it works even if there are lets in the hyps *)
+Goal exists e1 e2, Z.of_nat k = e1 * e2.
+intros. eexists. eexists.
+ match goal with |- _ = ?x * ?y =>
+ let Hx := fresh in
+ let Hy := fresh in
+ set (Hx:=x);
+ set (Hy:=y) end.
+(* Fail vm_compute. *)
+rewrite <- factorisable.
+evm blacklist [Zmult].
+unfold H, H0. reflexivity.
+Show Proof. Time Qed.
+
+
+
(* An example of a proof that blows up at Qed time, because the proof term does not provide enough information *)
(*
Check ("cbv without witnesses")%string.
@@ -77,4 +93,19 @@ rewrite <- factorisable.
set (f :=Z.mul).
Time cbv - [f]; unfold f; reflexivity. (* 4 s *)
Time Qed. (* 154 s !! *)
-*)
+*)
+
+Fixpoint nexists n P :=
+ match n with
+ | 0 => P
+ | S n => exists x, nexists n (P /\ x = 1)
+ end%nat.
+
+Check ("cbv with witnesses")%string.
+Goal exists e1 e2, nexists 10 (Z.of_nat k = e1 * e2).
+unfold nexists; do 12 eexists.
+rewrite <- (factorisable).
+evm blacklist [Zmult].
+repeat split.
+Time Qed.
+

0 comments on commit 2ef1dc5

Please sign in to comment.