diff options
Diffstat (limited to 'tactics/tauto.ml4')
| -rw-r--r-- | tactics/tauto.ml4 | 166 |
1 files changed, 116 insertions, 50 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 17ea121f..1729695d 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: tauto.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: tauto.ml4 11739 2009-01-02 19:33:19Z herbelin $ i*) open Term open Hipattern @@ -21,19 +21,44 @@ open Tacinterp open Tactics open Util -let assoc_last ist = - match List.assoc (Names.id_of_string "X1") ist.lfun with +let assoc_var s ist = + match List.assoc (Names.id_of_string s) ist.lfun with | VConstr c -> c | _ -> failwith "tauto: anomaly" +(** Parametrization of tauto *) + +(* Whether conjunction and disjunction are restricted to binary connectives *) +(* (this is the compatibility mode) *) +let binary_mode = true + +(* Whether conjunction and disjunction are restricted to the connectives *) +(* having the structure of "and" and "or" (up to the choice of sorts) in *) +(* contravariant position in an hypothesis (this is the compatibility mode) *) +let strict_in_contravariant_hyp = true + +(* Whether conjunction and disjunction are restricted to the connectives *) +(* having the structure of "and" and "or" (up to the choice of sorts) in *) +(* an hypothesis and in the conclusion *) +let strict_in_hyp_and_ccl = false + +(* Whether unit type includes equality types *) +let strict_unit = false + + +(** Test *) + let is_empty ist = - if is_empty_type (assoc_last ist) then + if is_empty_type (assoc_var "X1" ist) then <:tactic<idtac>> else <:tactic<fail>> -let is_unit ist = - if is_unit_type (assoc_last ist) then +(* Strictly speaking, this exceeds the propositional fragment as it + matches also equality types (and solves them if a reflexivity) *) +let is_unit_or_eq ist = + let test = if strict_unit then is_unit_type else is_unit_or_eq_type in + if test (assoc_var "X1" ist) then <:tactic<idtac>> else <:tactic<fail>> @@ -47,93 +72,138 @@ let is_record t = | _ -> false let is_binary t = + isApp t && let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in mib.Declarations.mind_nparams = 2 | _ -> false - + +let iter_tac tacl = + List.fold_right (fun tac tacs -> <:tactic< $tac; $tacs >>) tacl + +(** Dealing with conjunction *) + let is_conj ist = - let ind = assoc_last ist in - if (is_conjunction ind) && (is_nodep_ind ind) (* && not (is_record ind) *) - && is_binary ind (* for compatibility, as (?X _ _) matches - applications with 2 or more arguments. *) + let ind = assoc_var "X1" ist in + if (not binary_mode || is_binary ind) (* && not (is_record ind) *) + && is_conjunction ~strict:strict_in_hyp_and_ccl ind then <:tactic<idtac>> else <:tactic<fail>> +let flatten_contravariant_conj ist = + let typ = assoc_var "X1" ist in + let c = assoc_var "X2" ist in + match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with + | Some (_,args) -> + let i = List.length args in + if not binary_mode || i = 2 then + let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in + let intros = + iter_tac (List.map (fun _ -> <:tactic< intro >>) args) + <:tactic< idtac >> in + <:tactic< + let newtyp := $newtyp in + assert newtyp by ($intros; apply id; split; assumption); + clear id + >> + else + <:tactic<fail>> + | _ -> + <:tactic<fail>> + +(** Dealing with disjunction *) + let is_disj ist = - if is_disjunction (assoc_last ist) && is_binary (assoc_last ist) then + let t = assoc_var "X1" ist in + if (not binary_mode || is_binary t) && + is_disjunction ~strict:strict_in_hyp_and_ccl t + then <:tactic<idtac>> else <:tactic<fail>> +let flatten_contravariant_disj ist = + let typ = assoc_var "X1" ist in + let c = assoc_var "X2" ist in + match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with + | Some (_,args) -> + let i = List.length args in + if not binary_mode || i = 2 then + iter_tac (list_map_i (fun i arg -> + let typ = valueIn (VConstr (mkArrow arg c)) in + <:tactic< + let typ := $typ in + assert typ by (intro; apply id; constructor $i; assumption) + >>) 1 args) <:tactic< clear id >> + else + <:tactic<fail>> + | _ -> + <:tactic<fail>> + + +(** Main tactic *) + let not_dep_intros ist = <:tactic< repeat match goal with | |- (?X1 -> ?X2) => intro - | |- (Coq.Init.Logic.iff _ _) => unfold Coq.Init.Logic.iff - | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not - | H:(Coq.Init.Logic.iff _ _)|- _ => unfold Coq.Init.Logic.iff in H - | H:(Coq.Init.Logic.not _)|-_ => unfold Coq.Init.Logic.not in H - | H:(Coq.Init.Logic.iff _ _)->_|- _ => unfold Coq.Init.Logic.iff in H - | H:(Coq.Init.Logic.not _)->_|-_ => unfold Coq.Init.Logic.not in H + | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1 + | H:(Coq.Init.Logic.not _)|-_ => unfold Coq.Init.Logic.not at 1 in H + | H:(Coq.Init.Logic.not _)->_|-_ => unfold Coq.Init.Logic.not at 1 in H end >> let axioms ist = - let t_is_unit = tacticIn is_unit + let t_is_unit_or_eq = tacticIn is_unit_or_eq and t_is_empty = tacticIn is_empty in <:tactic< match reverse goal with - | |- ?X1 => $t_is_unit; constructor 1 + | |- ?X1 => $t_is_unit_or_eq; constructor 1 | _:?X1 |- _ => $t_is_empty; elimtype X1; assumption | _:?X1 |- ?X1 => assumption end >> let simplif ist = - let t_is_unit = tacticIn is_unit + let t_is_unit_or_eq = tacticIn is_unit_or_eq and t_is_conj = tacticIn is_conj + and t_flatten_contravariant_conj = tacticIn flatten_contravariant_conj + and t_flatten_contravariant_disj = tacticIn flatten_contravariant_disj and t_is_disj = tacticIn is_disj and t_not_dep_intros = tacticIn not_dep_intros in <:tactic< $t_not_dep_intros; repeat (match reverse goal with - | id: (?X1 _ _) |- _ => - $t_is_conj; elim id; do 2 intro; clear id - | id: (?X1 _ _) |- _ => $t_is_disj; elim id; intro; clear id + | id: ?X1 |- _ => $t_is_conj; elim id; do 2 intro; clear id + | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id + | id: ?X1 |- _ => $t_is_disj; elim id; intro; clear id | id0: ?X1-> ?X2, id1: ?X1|- _ => (* generalize (id0 id1); intro; clear id0 does not work (see Marco Maggiesi's bug PR#301) so we instead use Assert and exact. *) assert X2; [exact (id0 id1) | clear id0] | id: ?X1 -> ?X2|- _ => - $t_is_unit; cut X2; + $t_is_unit_or_eq; cut X2; [ intro; clear id | (* id : ?X1 -> ?X2 |- ?X2 *) cut X1; [exact id| constructor 1; fail] ] - | id: (?X1 ?X2 ?X3) -> ?X4|- _ => - $t_is_conj; cut (X2-> X3-> X4); - [ intro; clear id - | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X2 -> ?X3 -> ?X4 *) - intro; intro; cut (X1 X2 X3); [exact id| split; assumption] - ] - | id: (?X1 ?X2 ?X3) -> ?X4|- _ => - $t_is_disj; - cut (X3-> X4); - [cut (X2-> X4); - [intro; intro; clear id - | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X2 -> ?X4 *) - intro; cut (X1 X2 X3); [exact id| left; assumption] - ] - | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X3 -> ?X4 *) - intro; cut (X1 X2 X3); [exact id| right; assumption] - ] - | |- (?X1 _ _) => $t_is_conj; split + | id: ?X1 -> ?X2|- _ => + $t_flatten_contravariant_conj + (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *) + | id: (Coq.Init.Logic.iff ?X1 ?X2) -> ?X3|- _ => + assert ((X1 -> X2) -> (X2 -> X1) -> X3) + by (do 2 intro; apply id; split; assumption); + clear id + | id: ?X1 -> ?X2|- _ => + $t_flatten_contravariant_disj + (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2|-" and "?B->?X2|-" *) + | |- ?X1 => $t_is_conj; split + | |- (Coq.Init.Logic.iff _ _) => split end; $t_not_dep_intros) >> @@ -153,7 +223,7 @@ let rec tauto_intuit t_reduce solver ist = [ exact id | generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id; solve [ $t_tauto_intuit ]]] - | |- (?X1 _ _) => + | |- ?X1 => $t_is_disj; solve [left;$t_tauto_intuit | right;$t_tauto_intuit] end || @@ -164,13 +234,9 @@ let rec tauto_intuit t_reduce solver ist = || $t_solver ) >> - + let reduction_not_iff _ist = - <:tactic<repeat - match goal with - | |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff - | H:_ |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in H - end >> + <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >> let t_reduction_not_iff = tacticIn reduction_not_iff |