From be85b31e6817fe62a436b72bb96e0e936506d130 Mon Sep 17 00:00:00 2001 From: Olivier Laurent Date: Mon, 26 Apr 2021 21:39:47 +0200 Subject: [PATCH 1/3] apply reversible selection in auto-reverse mode --- proof.ml | 23 +++++++++++++++++++++++ sequent.ml | 2 ++ 2 files changed, 25 insertions(+) diff --git a/proof.ml b/proof.ml index 9721600..c0db2b9 100644 --- a/proof.ml +++ b/proof.ml @@ -223,6 +223,25 @@ let try_rule_request sequent rule_request = try from_sequent_and_rule_request sequent rule_request with Rule_exception _ -> raise NotApplicable;; +let is_atomic_zero_selection_sequent sequent = + let n = get_formula_position is_whynot sequent in + let head, _, tail = head_formula_tail n sequent in + List.for_all is_atomic_or_zero (head @ tail) + +let is_reversible_selection_sequent = function + | [f1; f2; Whynot _] when dual f1 = f2 -> false + | [f1; Whynot _; f2] when dual f1 = f2 -> false + | [Whynot _; f1; f2] when dual f1 = f2 -> false + | s -> is_atomic_zero_selection_sequent s + +let try_rule_selection sequent n = + let head, formula, tail = head_formula_tail n sequent in + match formula with + Whynot e -> Contraction_proof (head, e, tail, + (Dereliction_proof (head, e, Whynot e :: tail, + (Hypothesis_proof (head @ [e; Whynot e] @ tail))))) + | _ -> raise NotApplicable + let apply_reversible_rule proof = let sequent = get_conclusion proof in try try_rule_request sequent (Top (get_formula_position is_top sequent)) @@ -243,6 +262,10 @@ let apply_reversible_rule proof = with NotApplicable -> try try_rule_request sequent Axiom with NotApplicable -> + try if is_reversible_selection_sequent sequent + then try_rule_selection sequent (get_formula_position is_whynot sequent) + else raise NotApplicable + with NotApplicable -> proof;; let rec rec_apply_reversible_rule proof = diff --git a/sequent.ml b/sequent.ml index d6f38cd..1e12736 100644 --- a/sequent.ml +++ b/sequent.ml @@ -74,9 +74,11 @@ let get_unique_variable_names sequent = let is_top = function | Top -> true | _ -> false;; let is_bottom = function | Bottom -> true | _ -> false;; let is_par = function | Par _ -> true | _ -> false;; +let is_whynot = function | Whynot _ -> true | _ -> false;; let is_double_whynot = function | Whynot (Whynot _) -> true | _ -> false;; let is_with = function | With _ -> true | _ -> false;; let is_ofcourse = function | Ofcourse _ -> true | _ -> false;; +let is_atomic_or_zero = function | Litt _ | Dual _ | Zero -> true | _ -> false;; (* SEQUENT -> COQ *) From 7c6a9897e1269741d7775bbe3a2ebeee096c8d94 Mon Sep 17 00:00:00 2001 From: Olivier Laurent Date: Wed, 28 Apr 2021 21:50:40 +0200 Subject: [PATCH 2/3] at most one selection rule in auto_reverse --- auto_reverse_sequent.ml | 2 +- proof.ml | 36 +++++++++++++++++++----------------- 2 files changed, 20 insertions(+), 18 deletions(-) diff --git a/auto_reverse_sequent.ml b/auto_reverse_sequent.ml index b25f6e6..bd19ae8 100644 --- a/auto_reverse_sequent.ml +++ b/auto_reverse_sequent.ml @@ -1,6 +1,6 @@ let auto_reverse_sequent_with_exceptions request_as_json = let sequent = Raw_sequent.sequent_from_json request_as_json in - let proof = Proof.rec_apply_reversible_rule (Hypothesis_proof sequent) in + let proof = Proof.rec_apply_reversible_rule false (Hypothesis_proof sequent) in Proof.to_json proof;; let auto_reverse_sequent request_as_json = diff --git a/proof.ml b/proof.ml index c0db2b9..c8dc98f 100644 --- a/proof.ml +++ b/proof.ml @@ -242,38 +242,40 @@ let try_rule_selection sequent n = (Hypothesis_proof (head @ [e; Whynot e] @ tail))))) | _ -> raise NotApplicable -let apply_reversible_rule proof = +(* selection tells if selection rule already applied *) +let apply_reversible_rule selection proof = let sequent = get_conclusion proof in - try try_rule_request sequent (Top (get_formula_position is_top sequent)) + try try_rule_request sequent (Top (get_formula_position is_top sequent)), selection with NotApplicable -> - try try_rule_request sequent (Bottom (get_formula_position is_bottom sequent)) + try try_rule_request sequent (Bottom (get_formula_position is_bottom sequent)), selection with NotApplicable -> - try try_rule_request sequent (Par (get_formula_position is_par sequent)) + try try_rule_request sequent (Par (get_formula_position is_par sequent)), selection with NotApplicable -> - try try_rule_request sequent (Dereliction (get_formula_position is_double_whynot sequent)) + try try_rule_request sequent (Dereliction (get_formula_position is_double_whynot sequent)), selection with NotApplicable -> - try try_rule_request sequent (With (get_formula_position is_with sequent)) + try try_rule_request sequent (With (get_formula_position is_with sequent)), selection with NotApplicable -> - try try_rule_request sequent (Promotion (get_formula_position is_ofcourse sequent)) + try try_rule_request sequent (Promotion (get_formula_position is_ofcourse sequent)), selection with NotApplicable -> - try try_rule_request sequent One + try try_rule_request sequent One, selection with NotApplicable -> - try if List.length sequent = 1 then try_rule_request sequent (Tensor 0) else raise NotApplicable + try if List.length sequent = 1 then try_rule_request sequent (Tensor 0), selection + else raise NotApplicable with NotApplicable -> - try try_rule_request sequent Axiom + try try_rule_request sequent Axiom, selection with NotApplicable -> - try if is_reversible_selection_sequent sequent - then try_rule_selection sequent (get_formula_position is_whynot sequent) + try if not selection && is_reversible_selection_sequent sequent + then try_rule_selection sequent (get_formula_position is_whynot sequent), true else raise NotApplicable with NotApplicable -> - proof;; + proof, selection;; -let rec rec_apply_reversible_rule proof = - let new_proof = apply_reversible_rule proof in +let rec rec_apply_reversible_rule selection proof = + let new_proof, new_selection = apply_reversible_rule selection proof in match new_proof with | Hypothesis_proof _ -> new_proof | _ -> let premises = get_premises new_proof in - let new_premises = List.map rec_apply_reversible_rule premises in + let new_premises = List.map (rec_apply_reversible_rule new_selection) premises in set_premises new_proof new_premises;; (* PROOF -> RULE REQUEST *) @@ -483,4 +485,4 @@ let rec commute_permutations proof current_permutation = let new_proof = set_premises proof [commute_permutations p []] in if is_identity then new_proof else Exchange_proof (get_conclusion proof, perm, new_proof) | Exchange_proof (_, permutation, p) -> commute_permutations p (permute permutation perm) - | Hypothesis_proof s -> Hypothesis_proof (permute s perm);; \ No newline at end of file + | Hypothesis_proof s -> Hypothesis_proof (permute s perm);; From 33d880f21fd6e7c9e2615bfbdfb3f1f454e9476c Mon Sep 17 00:00:00 2001 From: Olivier Laurent Date: Fri, 30 Apr 2021 13:47:34 +0200 Subject: [PATCH 3/3] do not select already present formula in auto-reverse --- auto_reverse_sequent.ml | 4 +++- proof.ml | 5 +++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/auto_reverse_sequent.ml b/auto_reverse_sequent.ml index bd19ae8..3ff388f 100644 --- a/auto_reverse_sequent.ml +++ b/auto_reverse_sequent.ml @@ -1,6 +1,8 @@ +let auto_reverse_selection = true + let auto_reverse_sequent_with_exceptions request_as_json = let sequent = Raw_sequent.sequent_from_json request_as_json in - let proof = Proof.rec_apply_reversible_rule false (Hypothesis_proof sequent) in + let proof = Proof.rec_apply_reversible_rule (not auto_reverse_selection) (Hypothesis_proof sequent) in Proof.to_json proof;; let auto_reverse_sequent request_as_json = diff --git a/proof.ml b/proof.ml index c8dc98f..f2fb983 100644 --- a/proof.ml +++ b/proof.ml @@ -225,8 +225,9 @@ let try_rule_request sequent rule_request = let is_atomic_zero_selection_sequent sequent = let n = get_formula_position is_whynot sequent in - let head, _, tail = head_formula_tail n sequent in - List.for_all is_atomic_or_zero (head @ tail) + let head, formula, tail = head_formula_tail n sequent in + List.for_all is_atomic_or_zero (head @ tail) && + (not (List.mem formula sequent)) let is_reversible_selection_sequent = function | [f1; f2; Whynot _] when dual f1 = f2 -> false