diff options
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | contrib/subtac/FixSub.v | 78 | ||||
| -rw-r--r-- | contrib/subtac/FunctionalExtensionality.v | 26 | ||||
| -rw-r--r-- | contrib/subtac/Subtac.v | 2 | ||||
| -rw-r--r-- | contrib/subtac/Utils.v | 2 | ||||
| -rw-r--r-- | contrib/subtac/g_subtac.ml4 | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_cases.ml | 38 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 50 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.mli | 2 | ||||
| -rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 2 |
10 files changed, 165 insertions, 42 deletions
@@ -1076,7 +1076,8 @@ JPROVERVO= CCVO= -SUBTACVO=contrib/subtac/FixSub.vo contrib/subtac/Utils.vo +SUBTACVO=contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \ + contrib/subtac/FunctionalExtensionality.vo RTAUTOVO = \ contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v index ded069bf1..0016bfdaf 100644 --- a/contrib/subtac/FixSub.v +++ b/contrib/subtac/FixSub.v @@ -1,26 +1,76 @@ Require Import Wf. +Require Import Coq.subtac.Utils. Section Well_founded. -Variable A : Set. -Variable R : A -> A -> Prop. -Hypothesis Rwf : well_founded R. - -Section FixPoint. + Variable A : Set. + Variable R : A -> A -> Prop. + Hypothesis Rwf : well_founded R. + + Section Acc. + + Variable P : A -> Set. + + Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. + + Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x := + F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) + (Acc_inv r (proj1_sig y) (proj2_sig y))). + + Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). + End Acc. + + Section FixPoint. + Variable P : A -> Set. + + Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. + + Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) + + Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). + + Hypothesis + F_ext : + forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)), + (forall y:{ y:A | R y x}, f y = g y) -> F_sub x f = F_sub x g. -Variable P : A -> Set. + Lemma Fix_F_eq : + forall (x:A) (r:Acc R x), + F_sub x (fun (y:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r. + Proof. + destruct r using Acc_inv_dep; auto. + Qed. + + Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s. + Proof. + intro x; induction (Rwf x); intros. + rewrite <- (Fix_F_eq x r); rewrite <- (Fix_F_eq x s); intros. + apply F_ext; auto. + intros. + rewrite (proof_irrelevance (Acc R x) r s) ; auto. + Qed. -Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. - -Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x := - F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) - (Acc_inv r (proj1_sig y) (proj2_sig y))). + Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{y:A|R y x}) => Fix (proj1_sig y)). + Proof. + intro x; unfold Fix in |- *. + rewrite <- (Fix_F_eq ). + apply F_ext; intros. + apply Fix_F_inv. + Qed. -Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). + Lemma fix_sub_eq : + forall x : A, + Fix_sub P F_sub x = + let f_sub := F_sub in + f_sub x (fun {y : A | R y x}=> Fix (`y)). + exact Fix_eq. + Qed. -End FixPoint. + End FixPoint. End Well_founded. +Extraction Inline Fix_F_sub Fix_sub. + Require Import Wf_nat. Require Import Lt. @@ -44,3 +94,5 @@ Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (f x)). End FixPoint. End Well_founded_measure. + +Extraction Inline Fix_measure_F_sub Fix_measure_sub. diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v new file mode 100644 index 000000000..24c2f0142 --- /dev/null +++ b/contrib/subtac/FunctionalExtensionality.v @@ -0,0 +1,26 @@ +Axiom fun_extensionality : forall A B (f g : A -> B), + (forall x, f x = g x) -> f = g. + +Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), forall (f g : forall x : A, B x), + (forall x, f x = g x) -> f = g. + +Hint Resolve fun_extensionality fun_extensionality_dep : subtac. + +Require Import Coq.subtac.Utils. +Require Import Coq.subtac.FixSub. + +Lemma fix_sub_eq_ext : + forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) + (P : A -> Set) + (F_sub : forall x : A, (forall {y : A | R y x}, P (`y)) -> P x), + forall x : A, + Fix_sub A R Rwf P F_sub x = + let f_sub := F_sub in + F_sub x (fun {y : A | R y x}=> Fix A R Rwf P f_sub (`y)). +Proof. + intros ; apply Fix_eq ; auto. + intros. + assert(f = g). + apply (fun_extensionality_dep _ _ _ _ H). + rewrite H0 ; auto. +Qed. diff --git a/contrib/subtac/Subtac.v b/contrib/subtac/Subtac.v new file mode 100644 index 000000000..9912cd242 --- /dev/null +++ b/contrib/subtac/Subtac.v @@ -0,0 +1,2 @@ +Require Export Coq.subtac.Utils. +Require Export Coq.subtac.FixSub.
\ No newline at end of file diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index aa1d0ff38..6b613b0de 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -64,3 +64,5 @@ Ltac destruct_call f := end. Extraction Inline proj1_sig. + +Require Export ProofIrrelevance. diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 6f97a8eac..129ac75df 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -98,7 +98,9 @@ VERNAC COMMAND EXTEND Subtac_Obligations | [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, None) ] | [ "Obligation" integer(num) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, None, Some t) ] | [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None, None) ] - END +| [ "Next" "Obligation" "of" ident(name) ] -> [ Subtac_obligations.next_obligation (Some name) ] +| [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ] +END VERNAC COMMAND EXTEND Subtac_Solve_Obligations | [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ] diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 83e965d0a..e6404d7f2 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -716,9 +716,12 @@ let get_names env sign eqns = let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t)) +let all_name sign = List.map (fun (n, b, t) -> let n = match n with Name _ -> n | Anonymous -> Name (id_of_string "Anonymous") in + (n, b, t)) sign + let push_rels_eqn sign eqn = -(* trace (str "push_rels_eqn: " ++ my_print_rel_context eqn.rhs.rhs_env sign ++ *) -(* str " lift is " ++ int eqn.rhs.rhs_lift ++ *) + let sign = all_name sign in +(* trace (str "push_rels_eqn: " ++ my_print_rel_context eqn.rhs.rhs_env sign ++ str "end"); *) (* str " branch is " ++ my_print_constr (fst eqn.rhs.c_orig) (snd eqn.rhs.c_orig)); *) (* let rhs = eqn.rhs in *) (* let l, c, s, e = *) @@ -1201,9 +1204,13 @@ let build_leaf pb = | None -> anomaly "Predicate not found" | Some (PrCcl typ) -> mk_tycon typ | Some _ -> anomaly "not all parameters of pred have been consumed" in - (try trace (str "In build leaf: env is: " ++ my_print_env rhs.rhs_env) - with _ -> trace (str "Error in build leaf")); - tag, pb.typing_function tycon rhs.rhs_env rhs.it + (try trace (str "In build leaf:"); + trace (str "typing: " ++ my_print_rawconstr rhs.rhs_env rhs.it); + trace (str "env is: " ++ my_print_env rhs.rhs_env) + with _ -> trace (str "error")); + let x = tag, pb.typing_function tycon rhs.rhs_env rhs.it in + trace (str "end build leaf"); + x (* Building the sub-problem when all patterns are variables *) let shift_problem (current,t) pb = @@ -1720,22 +1727,27 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs = (try trace (str "branch env: " ++ print_env rhs_env) with _ -> trace (str "error in print branch env")); let tycon = lift_tycon (List.length eqs + signlen) tycon in + let j = typing_fun tycon rhs_env eqn.rhs.it in - (try trace (str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); + (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ + str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); with _ -> trace (str "Error in typed branch pretty printing")); let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in - (try trace (str "Branch decl: " ++ pr_rel_decl env branch_decl) + (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype)) with _ -> trace (str "Error in branch decl pp")); let branch = let bref = RVar (dummy_loc, branch_name) in - match vars_of_ctx rhs_rels with + match vars_of_ctx rhs_rels' with [] -> bref | l -> RApp (dummy_loc, bref, l) in + let branch = + List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels + in (try trace (str "New branch: " ++ Printer.pr_rawconstr branch) with _ -> trace (str "Error in new branch pp")); incr i; @@ -1791,7 +1803,8 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = (* Main entry of the matching compilation *) let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)= - + let env0 = env in + let tycon0 = tycon in (* We build the matrix of patterns and right-hand-side *) let matx = matx_of_eqns env tomatchl eqns in @@ -1801,6 +1814,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in let matx = List.rev matx in + trace (str "Old env: " ++ my_print_env env); let env = push_rels lets env in let len = List.length lets in let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in @@ -1831,10 +1845,12 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e let _, j = compile pb in (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; + let ty = out_some (valcon_of_tycon tycon0) in let j = { uj_val = it_mkLambda_or_LetIn (applistc j.uj_val args) lets; - uj_type = opred; } + uj_type = ty; } in - inh_conv_coerce_to_tycon loc env isevars j tycon + trace (str"final judgement:" ++ Prettyp.print_judgment env0 j ++ spc ()); + inh_conv_coerce_to_tycon loc env isevars j tycon0 end diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 5d982cf27..fd0d289e3 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -268,6 +268,25 @@ let deps_remaining obls deps = else x :: acc) deps [] +let solve_obligation prg num = + let user_num = succ num in + let obls, rem = prg.prg_obligations in + let obl = obls.(num) in + match deps_remaining obls obl.obl_deps with + [] -> + let obl = subst_deps_obl obls obl in + Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type + (fun strength gr -> + debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished"); + let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in + let obls = Array.copy obls in + let _ = obls.(num) <- obl in + update_obls prg obls (pred rem)); + Pfedit.by !default_tactic; + trace (str "Started obligation " ++ int user_num ++ str " proof") + | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " + ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) + let subtac_obligation (user_num, name, typ) = let num = pred user_num in let prg = get_prog name in @@ -275,21 +294,7 @@ let subtac_obligation (user_num, name, typ) = if num < Array.length obls then let obl = obls.(num) in match obl.obl_body with - None -> - (match deps_remaining obls obl.obl_deps with - [] -> - let obl = subst_deps_obl obls obl in - Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type - (fun strength gr -> - debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished"); - let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in - let obls = Array.copy obls in - let _ = obls.(num) <- obl in - update_obls prg obls (pred rem)); - Pfedit.by !default_tactic; - trace (str "Started obligation " ++ int user_num ++ str " proof") - | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " - ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))) + None -> solve_obligation prg num | Some r -> error "Obligation already solved" else error (sprintf "Unknown obligation number %i" (succ num)) @@ -344,6 +349,21 @@ let admit_obligations n = in update_obls prg obls' 0 +exception Found of int + +let array_find f arr = + try Array.iteri (fun i x -> if f x then raise (Found i)) arr; + raise Not_found + with Found i -> i + +let next_obligation n = + let prg = get_prog n in + let obls, rem = prg.prg_obligations in + let i = + array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) + obls + in + solve_obligation prg i open Pp let show_obligations n = diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 972aadce6..7953fb4b0 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -12,6 +12,8 @@ val add_mutual_definitions : val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit +val next_obligation : Names.identifier option -> unit + val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit val show_obligations : Names.identifier option -> unit diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 9339d7387..d9c193bed 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -326,7 +326,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let t = Retyping.get_type_of env sigma c in make_judge c t | _ -> resj in - inh_conv_coerce_to_tycon loc env isevars resj tycon + inh_conv_coerce_to_tycon loc env isevars resj tycon | RLambda(loc,name,c1,c2) -> let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in |