File Propositional
(* Order of Exports is important for mutable tacs *)
From MatchingLogic Require Export BasicProofSystemLemmas.
From MatchingLogic.ProofMode Require Export Basics.
Import MatchingLogic.Logic.Notations.
Lemma MLGoal_exactn {Σ : Signature}
(Γ : Theory)
(l₁ l₂ : hypotheses)
(name : string)
(g : Pattern)
(info : ProofInfo) :
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name g) :: l₂) g info.
Ltac2 do_mlExactn (n : constr) :=
do_ensureProofMode ();
do_mlReshapeHypsByIdx n;
Control.plus (fun () ⇒ apply MLGoal_exactn)
(fun _ ⇒ _mlReshapeHypsBack;
throw_pm_exn_with_goal "do_mlExactn: Hypothesis is not identical to the goal!")
.
Ltac2 Notation "mlExactn" n(constr) :=
do_mlExactn n
.
Tactic Notation "mlExactn" constr(n) :=
let f := ltac2:(n |- do_mlExactn (Option.get (Ltac1.to_constr n))) in
f n
.
Lemma MLGoal_exact {Σ : Signature} Γ l name g idx info:
find_hyp name l = Some (idx, (mkNH _ name g)) →
mkMLGoal Σ Γ l g info.
Ltac2 do_mlExact (name' : constr) :=
do_ensureProofMode ();
Control.plus (fun () ⇒
eapply MLGoal_exact with (name := $name');
simpl; apply f_equal; reflexivity)
(fun _ ⇒ _mlReshapeHypsBack;
throw_pm_exn_with_goal ("do_mlExact: Given hypothesis is not identical to the goal, or there is no pattern associated with the given name!"))
.
Ltac2 Notation "mlExact" name(constr) :=
do_mlExact name
.
Tactic Notation "mlExact" constr(name) :=
let f := ltac2:(name |- do_mlExact (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example ex_mlExact {Σ : Signature} Γ a b c:
well_formed a = true →
well_formed b = true →
well_formed c = true →
Γ ⊢i a ---> b ---> c ---> b using BasicReasoning.
Lemma MLGoal_weakenConclusion' {Σ : Signature} Γ l g g' (i : ProofInfo):
Γ ⊢i g ---> g' using i →
mkMLGoal Σ Γ l g i →
mkMLGoal Σ Γ l g' i.
Lemma prf_contraction {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ((a ---> a ---> b) ---> (a ---> b)) using BasicReasoning.
Lemma prf_weaken_conclusion_under_implication {Σ : Signature} Γ a b c:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i ((a ---> b) ---> ((a ---> (b ---> c)) ---> (a ---> c))) using BasicReasoning.
Lemma prf_weaken_conclusion_under_implication_meta {Σ : Signature} Γ a b c (i : ProofInfo):
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i (a ---> b) using i →
Γ ⊢i ((a ---> (b ---> c)) ---> (a ---> c)) using i.
Lemma prf_weaken_conclusion_under_implication_meta_meta {Σ : Signature} Γ a b c i:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i a ---> b using i →
Γ ⊢i a ---> b ---> c using i →
Γ ⊢i a ---> c using i.
Lemma prf_weaken_conclusion_iter_under_implication {Σ : Signature} Γ l g g':
Pattern.wf l →
well_formed g →
well_formed g' →
Γ ⊢i (((g ---> g') ---> (foldr patt_imp g l)) ---> ((g ---> g') ---> (foldr patt_imp g' l)))
using BasicReasoning.
Lemma prf_weaken_conclusion_iter_under_implication_meta {Σ : Signature} Γ l g g' (i : ProofInfo):
Pattern.wf l →
well_formed g →
well_formed g' →
Γ ⊢i ((g ---> g') ---> (foldr patt_imp g l)) using i→
Γ ⊢i ((g ---> g') ---> (foldr patt_imp g' l)) using i.
Lemma MLGoal_weakenConclusion_under_first_implication {Σ : Signature} Γ l name g g' i:
mkMLGoal Σ Γ (mkNH _ name (g ---> g') :: l) g i →
mkMLGoal Σ Γ (mkNH _ name (g ---> g') :: l) g' i .
Lemma prf_weaken_conclusion_iter_under_implication_iter {Σ : Signature} Γ l₁ l₂ g g':
Pattern.wf l₁ →
Pattern.wf l₂ →
well_formed g →
well_formed g' →
Γ ⊢i ((foldr patt_imp g (l₁ ++ (g ---> g') :: l₂)) --->
(foldr patt_imp g' (l₁ ++ (g ---> g') :: l₂)))
using BasicReasoning.
Lemma prf_weaken_conclusion_iter_under_implication_iter_meta {Σ : Signature} Γ l₁ l₂ g g' i:
Pattern.wf l₁ →
Pattern.wf l₂ →
well_formed g →
well_formed g' →
Γ ⊢i (foldr patt_imp g (l₁ ++ (g ---> g') :: l₂)) using i →
Γ ⊢i (foldr patt_imp g' (l₁ ++ (g ---> g') :: l₂)) using i.
Lemma MLGoal_weakenConclusion {Σ : Signature} Γ l₁ l₂ name g g' i:
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name (g ---> g')) :: l₂) g i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name (g ---> g')) :: l₂) g' i.
Ltac2 run_in_reshaped_by_idx
(n : constr) (f : unit → unit) : unit :=
do_ensureProofMode ();
do_mlReshapeHypsByIdx n;
f ();
do_mlReshapeHypsBack ()
.
Ltac2 do_mlApplyn (n : constr) :=
run_in_reshaped_by_idx n ( fun () ⇒
Control.plus (fun () ⇒ apply MLGoal_weakenConclusion)
(fun _ ⇒ throw_pm_exn_with_goal "do_mlApplyn: Failed for goal: ")
)
.
Ltac2 Notation "mlApplyn" n(constr) :=
do_mlApplyn n
.
Tactic Notation "mlApplyn" constr(n) :=
let f := ltac2:(n |- do_mlApplyn (Option.get (Ltac1.to_constr n))) in
f n
.
Ltac2 run_in_reshaped_by_name
(name : constr) (f : unit → unit) : unit :=
do_ensureProofMode ();
do_mlReshapeHypsByName name;
f ();
do_mlReshapeHypsBack ()
.
Ltac2 do_mlApply (name' : constr) :=
run_in_reshaped_by_name name' (fun () ⇒
Control.plus (fun () ⇒ apply MLGoal_weakenConclusion)
(fun _ ⇒ throw_pm_exn_with_goal "do_mlApply: Goal does not match the conclusion of the hypothesis")
)
.
Ltac2 Notation "mlApply" name(constr) :=
do_mlApply name
.
Tactic Notation "mlApply" constr(name') :=
let f := ltac2:(name' |- do_mlApply (Option.get (Ltac1.to_constr name'))) in
f name'
.
Local Example ex_mlApplyn {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i a ---> (a ---> b) ---> b using BasicReasoning.
Lemma Constructive_dilemma {Σ : Signature} Γ p q r s:
well_formed p →
well_formed q →
well_formed r →
well_formed s →
Γ ⊢i ((p ---> q) ---> (r ---> s) ---> (p or r) ---> (q or s)) using BasicReasoning.
Lemma prf_impl_distr_meta {Σ : Signature} Γ a b c i:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i (a ---> (b ---> c)) using i →
Γ ⊢i ((a ---> b) ---> (a ---> c)) using i.
Lemma prf_add_lemma_under_implication {Σ : Signature} Γ l g h:
Pattern.wf l →
well_formed g →
well_formed h →
Γ ⊢i ((foldr patt_imp h l) --->
((foldr patt_imp g (l ++ [h])) --->
(foldr patt_imp g l)))
using BasicReasoning.
Lemma prf_add_lemma_under_implication_meta {Σ : Signature} Γ l g h i:
Pattern.wf l →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp h l) using i →
Γ ⊢i ((foldr patt_imp g (l ++ [h])) ---> (foldr patt_imp g l)) using i.
Lemma prf_add_lemma_under_implication_meta_meta {Σ : Signature} Γ l g h i:
Pattern.wf l →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp h l) using i →
Γ ⊢i (foldr patt_imp g (l ++ [h])) using i →
Γ ⊢i (foldr patt_imp g l) using i.
Lemma mlGoal_assert {Σ : Signature} Γ l name g h i:
well_formed h →
mkMLGoal Σ Γ l h i →
mkMLGoal Σ Γ (l ++ [mkNH _ name h]) g i →
mkMLGoal Σ Γ l g i.
Lemma impl_elim
{Σ: Signature}
(Γ : Theory)
(A B C : Pattern)
(l1 l2 : list Pattern)
(i : ProofInfo)
:
Γ ⊢i foldr patt_imp A (l1 ++ l2) using i →
Γ ⊢i foldr patt_imp C (l1 ++ B :: l2) using i →
Γ ⊢i foldr patt_imp C (l1 ++ (A ---> B)::l2) using i
.
Lemma mlGoal_destructImp {Σ : Signature} Γ l1 l2 name C A B i:
mkMLGoal Σ Γ (l1 ++ l2) A i →
mkMLGoal Σ Γ (l1 ++ (mkNH _ name B)::l2) C i →
mkMLGoal Σ Γ (l1 ++ (mkNH _ name (A ---> B))::l2) C i.
Ltac2 do_mlDestructImp (name : constr) :=
run_in_reshaped_by_name name (fun () ⇒
Control.plus (fun () ⇒ apply (mlGoal_destructImp _ _ _ $name))
(fun _ ⇒ throw_pm_exn_with_goal "do_mlDestructImp: The given hypothesis was not an implication pattern: ")
)
.
Ltac2 Notation "mlDestructImp" name(constr) :=
do_mlDestructImp name
.
Tactic Notation "mlDestructImp" constr(name) :=
let f := ltac2:(name |- do_mlDestructImp (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example Test_destructImp {Σ : Signature} Γ :
∀ A B C, well_formed A → well_formed B → well_formed C →
Γ ⊢i (A ---> B) ---> (B ---> C) ---> A ---> C using BasicReasoning.
Lemma MLGoal_revert {Σ : Signature} (Γ : Theory) (l1 l2 : hypotheses) (x g : Pattern) (n : string) i :
mkMLGoal Σ Γ (l1 ++ l2) (x ---> g) i →
mkMLGoal Σ Γ (l1 ++ (mkNH _ n x) :: l2) g i.
Ltac2 do_mlRevert (name : constr) :=
run_in_reshaped_by_name name (fun () ⇒
Control.plus (fun () ⇒ apply (MLGoal_revert _ _ _ _ _ $name))
(fun _ ⇒ throw_pm_exn_with_goal "do_mlRevert: failed for goal: ")
)
.
Ltac2 Notation "mlRevert" name(constr) :=
do_mlRevert name
.
Tactic Notation "mlRevert" constr(name) :=
let f := ltac2:(name |- do_mlRevert (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example Test_revert {Σ : Signature} Γ :
∀ A B C, well_formed A → well_formed B → well_formed C →
Γ ⊢i A ---> B ---> C ---> A using BasicReasoning.
Lemma prf_add_lemma_under_implication_generalized {Σ : Signature} Γ l1 l2 g h:
Pattern.wf l1 →
Pattern.wf l2 →
well_formed g →
well_formed h →
Γ ⊢i ((foldr patt_imp h l1) ---> ((foldr patt_imp g (l1 ++ [h] ++ l2)) ---> (foldr patt_imp g (l1 ++ l2))))
using BasicReasoning.
Lemma prf_add_lemma_under_implication_generalized_meta {Σ : Signature} Γ l1 l2 g h i:
Pattern.wf l1 →
Pattern.wf l2 →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp h l1) using i →
Γ ⊢i ((foldr patt_imp g (l1 ++ [h] ++ l2)) ---> (foldr patt_imp g (l1 ++ l2))) using i.
Lemma prf_add_lemma_under_implication_generalized_meta_meta {Σ : Signature} Γ l1 l2 g h i:
Pattern.wf l1 →
Pattern.wf l2 →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp h l1) using i →
Γ ⊢i (foldr patt_imp g (l1 ++ [h] ++ l2)) using i →
Γ ⊢i (foldr patt_imp g (l1 ++ l2)) using i.
Lemma mlGoal_assert_generalized {Σ : Signature} Γ l1 l2 name g h i:
well_formed h →
mkMLGoal Σ Γ l1 h i →
mkMLGoal Σ Γ (l1 ++ [mkNH _ name h] ++ l2) g i →
mkMLGoal Σ Γ (l1 ++ l2) g i.
Ltac2 do_mlAssert_nocheck
(name : constr) (t : constr) :=
lazy_match! goal with
| [ |- @of_MLGoal _ (@mkMLGoal ?sgm ?ctx ?l ?g ?i)] ⇒
let hwf := Fresh.in_goal ident:(Hwf) in
assert ($hwf : well_formed $t = true) >
[()|(
let hwf_constr := Control.hyp hwf in
let h := Fresh.in_goal ident:(H) in
assert ($h : @of_MLGoal $sgm (@mkMLGoal $sgm $ctx $l $t $i)) >
[() |
let h_constr := Control.hyp h in
(eapply (@mlGoal_assert $sgm $ctx $l $name $g $t $i $hwf_constr $h_constr);
ltac1:(rewrite [_ ++ _]/=); clear $h)]
)]
end.
Ltac2 Notation "_mlAssert_nocheck" "(" name(constr) ":" t(constr) ")" :=
do_mlAssert_nocheck name t
.
Tactic Notation "_mlAssert_nocheck" "(" constr(name) ":" constr(t) ")" :=
let f := ltac2:(name t |- do_mlAssert_nocheck (Option.get (Ltac1.to_constr name)) (Option.get (Ltac1.to_constr t))) in
f name t
.
Ltac2 do_mlAssert (name : constr) (t : constr) :=
do_ensureProofMode ();
do_failIfUsed name;
do_mlAssert_nocheck name t
.
Ltac2 Notation "mlAssert" "(" name(constr) ":" t(constr) ")" :=
do_mlAssert name t
.
(* TODO: make this bind tigther. *)
Tactic Notation "mlAssert" "(" constr(name) ":" constr(t) ")" :=
let f := ltac2:(name t |- do_mlAssert (Option.get (Ltac1.to_constr name)) (Option.get (Ltac1.to_constr t))) in
f name t
.
Ltac2 do_mlAssert_autonamed (t : constr) :=
do_ensureProofMode ();
let hyps := do_getHypNames () in
let name := eval lazy in (fresh $hyps) in
do_mlAssert name t
.
Ltac2 Notation "mlAssert" "(" t(constr) ")" :=
do_mlAssert_autonamed t
.
Tactic Notation "mlAssert" "(" constr(t) ")" :=
let f := ltac2:(t |- do_mlAssert_autonamed (Option.get (Ltac1.to_constr t))) in
f t
.
Local Example ex_mlAssert {Σ : Signature} Γ a:
well_formed a →
Γ ⊢i (a ---> a ---> a) using BasicReasoning.
Ltac2 _getGoalProofInfo () : constr :=
lazy_match! goal with
| [|- @of_MLGoal _ (@mkMLGoal _ _ _ _ ?i)]
⇒ i
end.
Ltac2 _getGoalTheory () : constr :=
lazy_match! goal with
| [|- @of_MLGoal _ (@mkMLGoal _ ?ctx _ _ _)]
⇒ ctx
end.
Ltac2 mlAssert_using_first
(name : constr) (t : constr) (n : constr) :=
do_ensureProofMode ();
do_failIfUsed name;
lazy_match! goal with
| [|- @of_MLGoal ?sgm (@mkMLGoal ?sgm ?ctx ?l ?g ?i)] ⇒
let l1 := Fresh.in_goal ident:(l1) in
let l2 := Fresh.in_goal ident:(l2) in
let heql1 := Fresh.in_goal ident:(Heql1) in
let heql2 := Fresh.in_goal ident:(Heql2) in
remember (take $n $l) as l1 eqn:$heql1 in |-;
remember (drop $n $l) as l2 eqn:$heql2 in |-;
simpl in Heql1; simpl in Heql2;
eapply cast_proof_ml_hyps >
[(
ltac1:(l n |- rewrite -[l](take_drop n)) (Ltac1.of_constr l) (Ltac1.of_constr n);
reflexivity
)|()];
let hwf := Fresh.in_goal ident:(Hwf) in
assert ($hwf : well_formed $t = true) >
[()|
let h := Fresh.in_goal ident:(H) in
let l1_constr := Control.hyp l1 in
(* let l2_constr := Control.hyp l2 in *)
let heql1_constr := Control.hyp heql1 in
let hwf_constr := Control.hyp hwf in
assert ($h : @of_MLGoal $sgm (@mkMLGoal $sgm $ctx $l1_constr $t $i)) >
[
(eapply cast_proof_ml_hyps>
[(rewrite → $heql1_constr; reflexivity)|()]);
clear $l1 $l2 $heql1 $heql2
|
let h_constr := Control.hyp h in
apply (cast_proof_ml_hyps _ _ _ (f_equal patterns_of $heql1_constr)) in $h;
eapply (@mlGoal_assert_generalized $sgm $ctx (take $n $l) (drop $n $l) $name $g $t $i $hwf_constr $h_constr);
ltac1:(rewrite [_ ++ _]/=);
clear $l1 $l2 $heql1 $heql2 $h
]
]
end.
Ltac2 Notation "mlAssert" "(" name(constr) ":" t(constr) ")" "using" "first" n(constr) :=
mlAssert_using_first name t n
.
Tactic Notation "mlAssert" "(" constr(name) ":" constr(t) ")" "using" "first" constr(n) :=
let f := ltac2:(name t n |- mlAssert_using_first (Option.get (Ltac1.to_constr name)) (Option.get (Ltac1.to_constr t)) (Option.get (Ltac1.to_constr n))) in
f name t n
.
Ltac2 mlAssert_autonamed_using_first
(t : constr) (n : constr) :=
do_ensureProofMode ();
let hyps := do_getHypNames () in
let name := eval cbv in (fresh $hyps) in
mlAssert_using_first name t n
.
Ltac2 Notation "mlAssert" "(" t(constr) ")" "using" "first" n(constr) :=
mlAssert_autonamed_using_first t n
.
Tactic Notation "mlAssert" "(" constr(t) ")" "using" "first" constr(n) :=
let f := ltac2:(t n |- mlAssert_autonamed_using_first (Option.get (Ltac1.to_constr t)) (Option.get (Ltac1.to_constr n))) in
f t n
.
Local Example ex_assert_using {Σ : Signature} Γ p q a b:
well_formed a = true →
well_formed b = true →
well_formed p = true →
well_formed q = true →
Γ ⊢i a ---> p and q ---> b ---> ! ! q using BasicReasoning.
Lemma P4i' {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i ((!A ---> A) ---> A) using BasicReasoning.
Lemma tofold {Σ : Signature} p:
p = fold_right patt_imp p [].
Lemma consume {Σ : Signature} p q l:
fold_right patt_imp (p ---> q) l = fold_right patt_imp q (l ++ [p]).
Lemma prf_disj_elim {Σ : Signature} Γ p q r:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i ((p ---> r) ---> (q ---> r) ---> (p or q) ---> r)
using BasicReasoning.
Lemma prf_disj_elim_meta {Σ : Signature} Γ p q r i:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i (p ---> r) using i →
Γ ⊢i ((q ---> r) ---> (p or q) ---> r) using i.
Lemma prf_disj_elim_meta_meta {Σ : Signature} Γ p q r i:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i (p ---> r) using i →
Γ ⊢i (q ---> r) using i →
Γ ⊢i ((p or q) ---> r) using i.
Lemma prf_disj_elim_meta_meta_meta {Σ : Signature} Γ p q r i:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i (p ---> r) using i →
Γ ⊢i (q ---> r) using i →
Γ ⊢i (p or q) using i →
Γ ⊢i r using i.
Lemma prf_add_proved_to_assumptions {Σ : Signature} Γ l a g i:
Pattern.wf l →
well_formed a →
well_formed g →
Γ ⊢i a using i→
Γ ⊢i ((foldr patt_imp g (a::l)) ---> (foldr patt_imp g l)) using i.
Lemma prf_add_proved_to_assumptions_meta {Σ : Signature} Γ l a g i:
Pattern.wf l →
well_formed a →
well_formed g →
Γ ⊢i a using i →
Γ ⊢i (foldr patt_imp g (a::l)) using i →
Γ ⊢i (foldr patt_imp g l) using i.
Lemma MLGoal_add {Σ : Signature} Γ l name g h i:
Γ ⊢i h using i →
mkMLGoal Σ Γ (mkNH _ name h::l) g i →
mkMLGoal Σ Γ l g i.
Ltac2 do_mlAdd_as (n : constr) (name' : constr) :=
do_ensureProofMode ();
do_failIfUsed name';
lazy_match! goal with
| [|- @of_MLGoal ?sgm (@mkMLGoal ?sgm ?ctx ?l ?g ?i)] ⇒
Control.plus(fun () ⇒
apply (@MLGoal_add $sgm $ctx $l $name' $g _ $i $n)
)
(fun _ ⇒ throw_pm_exn (Message.concat (Message.of_string "do_mlAdd_as: given Coq hypothesis is not a pattern: ") (Message.of_constr n)))
end.
Ltac2 Notation "mlAdd" n(constr) "as" name(constr) :=
do_mlAdd_as n name
.
Tactic Notation "mlAdd" constr(n) "as" constr(name') :=
let f := ltac2:(n name |- do_mlAdd_as (Option.get (Ltac1.to_constr n)) (Option.get (Ltac1.to_constr name))) in
f n name'
.
Ltac2 get_fresh_name () : constr :=
do_ensureProofMode ();
let hyps := do_getHypNames () in
let name := eval cbv in (fresh $hyps) in
name
.
Ltac2 do_mlAdd (n : constr) :=
do_mlAdd_as n (get_fresh_name ())
.
Ltac2 Notation "mlAdd" n(constr) :=
do_mlAdd n
.
Tactic Notation "mlAdd" constr(n) :=
let f := ltac2:(n |- do_mlAdd (Option.get (Ltac1.to_constr n))) in
f n
.
Local Example ex_mlAdd {Σ : Signature} Γ l g h i:
Pattern.wf l →
well_formed g →
well_formed h →
Γ ⊢i (h ---> g) using i →
Γ ⊢i h using i →
Γ ⊢i g using i.
Lemma prf_clear_hyp {Σ : Signature} Γ l1 l2 g h:
Pattern.wf l1 →
Pattern.wf l2 →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp g (l1 ++ l2)) ---> (foldr patt_imp g (l1 ++ [h] ++ l2))
using BasicReasoning.
Lemma prf_clear_hyp_meta {Σ : Signature} Γ l1 l2 g h i:
Pattern.wf l1 →
Pattern.wf l2 →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp g (l1 ++ l2)) using i →
Γ ⊢i (foldr patt_imp g (l1 ++ [h] ++ l2)) using i.
Lemma mlGoal_clear_hyp {Σ : Signature} Γ l1 l2 g h i:
mkMLGoal Σ Γ (l1 ++ l2) g i →
mkMLGoal Σ Γ (l1 ++ h::l2) g i.
Ltac2 do_mlClear (name : constr) :=
run_in_reshaped_by_name name (fun () ⇒
apply mlGoal_clear_hyp
)
.
Ltac2 Notation "mlClear" name(constr) :=
do_mlClear name
.
Tactic Notation "mlClear" constr(name) :=
let f := ltac2:(name |- do_mlClear (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example ex_mlClear {Σ : Signature} Γ a b c:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i a ---> (b ---> (c ---> b)) using BasicReasoning.
Lemma not_concl {Σ : Signature} Γ p q:
well_formed p →
well_formed q →
Γ ⊢i (p ---> (q ---> ((p ---> ! q) ---> ⊥))) using BasicReasoning.
Lemma reorder_last_to_head {Σ : Signature} Γ g x l:
Pattern.wf l →
well_formed g →
well_formed x →
Γ ⊢i ((foldr patt_imp g (x::l)) ---> (foldr patt_imp g (l ++ [x]))) using BasicReasoning.
Lemma reorder_last_to_head_meta {Σ : Signature} Γ g x l i:
Pattern.wf l →
well_formed g →
well_formed x →
Γ ⊢i (foldr patt_imp g (x::l)) using i →
Γ ⊢i (foldr patt_imp g (l ++ [x])) using i.
(* Iterated modus ponens.
For l = x₁, ..., xₙ, it says that
Γ ⊢i ((x₁ -> ... -> xₙ -> (x₁ -> ... -> xₙ -> r)) -> r)
*)
Lemma modus_ponens_iter {Σ : Signature} Γ l r:
Pattern.wf l →
well_formed r →
Γ ⊢i (foldr patt_imp r (l ++ [foldr patt_imp r l])) using BasicReasoning.
Lemma and_impl {Σ : Signature} Γ p q r:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i ((p and q ---> r) ---> (p ---> (q ---> r))) using BasicReasoning.
Lemma and_impl' {Σ : Signature} Γ p q r:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i ((p ---> (q ---> r)) ---> ((p and q) ---> r)) using BasicReasoning.
Lemma prf_disj_elim_iter {Σ : Signature} Γ l p q r:
Pattern.wf l →
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i ((fold_right patt_imp r (l ++ [p]))
--->
((fold_right patt_imp r (l ++ [q]))
--->
(fold_right patt_imp r (l ++ [p or q]))))
using BasicReasoning.
Lemma prf_disj_elim_iter_2 {Σ : Signature} Γ l₁ l₂ p q r:
Pattern.wf l₁ →
Pattern.wf l₂ →
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i ((fold_right patt_imp r (l₁ ++ [p] ++ l₂))
--->
((fold_right patt_imp r (l₁ ++ [q] ++ l₂))
--->
(fold_right patt_imp r (l₁ ++ [p or q] ++ l₂))))
using BasicReasoning.
Lemma prf_disj_elim_iter_2_meta {Σ : Signature} Γ l₁ l₂ p q r i:
Pattern.wf l₁ →
Pattern.wf l₂ →
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i (fold_right patt_imp r (l₁ ++ [p] ++ l₂)) using i →
Γ ⊢i ((fold_right patt_imp r (l₁ ++ [q] ++ l₂))
--->
(fold_right patt_imp r (l₁ ++ [p or q] ++ l₂))) using i.
Lemma prf_disj_elim_iter_2_meta_meta {Σ : Signature} Γ l₁ l₂ p q r i:
Pattern.wf l₁ →
Pattern.wf l₂ →
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i (fold_right patt_imp r (l₁ ++ [p] ++ l₂)) using i →
Γ ⊢i (fold_right patt_imp r (l₁ ++ [q] ++ l₂)) using i →
Γ ⊢i (fold_right patt_imp r (l₁ ++ [p or q] ++ l₂)) using i.
Lemma MLGoal_disj_elim {Σ : Signature} Γ l₁ l₂ pn p qn q pqn r i:
mkMLGoal Σ Γ (l₁ ++ (mkNH _ pn p) :: l₂) r i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ qn q) :: l₂) r i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ pqn (p or q)) :: l₂) r i.
Ltac2 do_mlDestructOr_as (name : constr) (name1 : constr) (name2 : constr) :=
do_ensureProofMode ();
do_failIfUsed name1;
do_failIfUsed name2;
lazy_match! goal with
| [|- @of_MLGoal _ (@mkMLGoal _ _ _ _ _)] ⇒
(* let htd := Fresh.in_goal ident:(Htd) in *)
eapply cast_proof_ml_hyps;
f_equal;
_mlReshapeHypsByName name;
Control.plus (fun () ⇒
apply MLGoal_disj_elim with (pqn := $name) (pn := $name1) (qn := $name2);
_mlReshapeHypsBack
)
(fun _ ⇒ _mlReshapeHypsBack;
throw_pm_exn_with_goal "do_mlDestructOr_as: failed for goal: ")
end
.
Ltac2 Notation "mlDestructOr" name(constr) "as" name1(constr) name2(constr) :=
do_mlDestructOr_as name name1 name2
.
Tactic Notation "mlDestructOr" constr(name) "as" constr(name1) constr(name2) :=
let f := ltac2:(name name1 name2 |- do_mlDestructOr_as (Option.get (Ltac1.to_constr name)) (Option.get (Ltac1.to_constr name1)) (Option.get (Ltac1.to_constr name2))) in
f name name1 name2
.
Ltac2 do_mlDestructOr (name : constr) :=
do_ensureProofMode ();
let hyps := do_getHypNames () in
let name0 := eval cbv in (fresh $hyps) in
let name1 := eval cbv in (fresh ($name0 :: $hyps)) in
mlDestructOr $name as $name0 $name1
.
Ltac2 Notation "mlDestructOr" name(constr) :=
do_mlDestructOr name
.
Tactic Notation "mlDestructOr" constr(name) :=
let f := ltac2:(name |- do_mlDestructOr (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example exd {Σ : Signature} Γ a b p q c i:
well_formed a →
well_formed b →
well_formed p →
well_formed q →
well_formed c →
Γ ⊢i (a ---> p ---> b ---> c) using i →
Γ ⊢i (a ---> q ---> b ---> c) using i→
Γ ⊢i (a ---> (p or q) ---> b ---> c) using i.
Lemma pf_iff_split {Σ : Signature} Γ A B i:
well_formed A →
well_formed B →
Γ ⊢i A ---> B using i →
Γ ⊢i B ---> A using i →
Γ ⊢i A <---> B using i.
Lemma pf_iff_proj1 {Σ : Signature} Γ A B i:
well_formed A →
well_formed B →
Γ ⊢i A <---> B using i →
Γ ⊢i A ---> B using i.
Lemma pf_iff_proj2 {Σ : Signature} Γ A B i:
well_formed A →
well_formed B →
Γ ⊢i (A <---> B) using i →
Γ ⊢i (B ---> A) using i.
Lemma pf_iff_iff {Σ : Signature} Γ A B i:
well_formed A →
well_formed B →
prod ((Γ ⊢i (A <---> B) using i) → (prod (Γ ⊢i (A ---> B) using i) (Γ ⊢i (B ---> A) using i)))
( (prod (Γ ⊢i (A ---> B) using i) (Γ ⊢i (B ---> A) using i)) → (Γ ⊢i (A <---> B) using i)).
Lemma pf_iff_equiv_refl {Σ : Signature} Γ A :
well_formed A →
Γ ⊢i (A <---> A) using BasicReasoning.
Lemma pf_iff_equiv_sym {Σ : Signature} Γ A B i:
well_formed A →
well_formed B →
Γ ⊢i (A <---> B) using i →
Γ ⊢i (B <---> A) using i.
Lemma pf_iff_equiv_trans {Σ : Signature} Γ A B C i:
well_formed A →
well_formed B →
well_formed C →
Γ ⊢i (A <---> B) using i →
Γ ⊢i (B <---> C) using i →
Γ ⊢i (A <---> C) using i.
Lemma prf_conclusion {Σ : Signature} Γ a b i:
well_formed a →
well_formed b →
Γ ⊢i b using i →
Γ ⊢i (a ---> b) using i.
Lemma and_of_negated_iff_not_impl {Σ : Signature} Γ p1 p2:
well_formed p1 →
well_formed p2 →
Γ ⊢i (! (! p1 ---> p2) <---> ! p1 and ! p2)
using BasicReasoning.
Lemma and_impl_2 {Σ : Signature} Γ p1 p2:
well_formed p1 →
well_formed p2 →
Γ ⊢i (! (p1 ---> p2) <---> p1 and ! p2)
using BasicReasoning.
Lemma conj_intro_meta_partial {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A → well_formed B →
Γ ⊢i A using i →
Γ ⊢i B ---> (A and B) using i.
Lemma and_impl_patt {Σ : Signature} (A B C : Pattern) Γ (i : ProofInfo):
well_formed A → well_formed B → well_formed C →
Γ ⊢i A using i →
Γ ⊢i ((A and B) ---> C) using i →
Γ ⊢i (B ---> C) using i.
Lemma conj_intro2 {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A → well_formed B →
Γ ⊢i (A ---> (B ---> (B and A)))
using BasicReasoning.
Lemma conj_intro_meta_partial2 {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo):
well_formed A → well_formed B →
Γ ⊢i A using i →
Γ ⊢i B ---> (B and A) using i.
Lemma and_impl_patt2 {Σ : Signature} (A B C : Pattern) Γ (i : ProofInfo):
well_formed A → well_formed B → well_formed C →
Γ ⊢i A using i →
Γ ⊢i ((B and A) ---> C) using i →
Γ ⊢i (B ---> C) using i.
Lemma patt_and_comm_meta {Σ : Signature} (A B : Pattern) (Γ : Theory) (i : ProofInfo) :
well_formed A → well_formed B
→
Γ ⊢i A and B using i →
Γ ⊢i B and A using i.
Lemma MLGoal_applyMeta {Σ : Signature} Γ r r' i:
Γ ⊢i (r' ---> r) using i →
∀ l,
mkMLGoal Σ Γ l r' i →
mkMLGoal Σ Γ l r i.
(* Error message of this one is sufficient *)
Ltac2 do_mlApplyMetaRaw (t : constr) :=
eapply (@MLGoal_applyMeta _ _ _ _ _ $t)
.
Ltac2 Notation "_mlApplyMetaRaw" t(open_constr) :=
do_mlApplyMetaRaw t
.
Tactic Notation "_mlApplyMetaRaw" uconstr(t) :=
let f := ltac2:(t |- do_mlApplyMetaRaw (Option.get (Ltac1.to_constr t))) in
f t
.
Lemma MLGoal_left {Σ : Signature} Γ l x y i:
mkMLGoal Σ Γ l x i →
mkMLGoal Σ Γ l (patt_or x y) i.
Lemma MLGoal_right {Σ : Signature} Γ l x y i:
mkMLGoal Σ Γ l y i →
mkMLGoal Σ Γ l (patt_or x y) i.
Ltac2 mlLeft () :=
_ensureProofMode;
Control.plus(fun () ⇒
apply MLGoal_left
)
(fun _ ⇒ throw_pm_exn_with_goal "mlLeft: Current matching logic goal is not a disjunction! ")
.
Ltac2 mlRight () :=
_ensureProofMode;
Control.plus(fun () ⇒
apply MLGoal_right
)
(fun _ ⇒ throw_pm_exn_with_goal "mlLeft: Current matching logic goal is not a disjunction! ")
.
Ltac mlLeft := ltac2:(mlLeft ()).
Ltac mlRight := ltac2:(mlRight ()).
Local Example ex_mlLeft {Σ : Signature} Γ a:
well_formed a →
Γ ⊢i a ---> (a or a)
using BasicReasoning.
Lemma MLGoal_applyMetaIn {Σ : Signature} Γ n r n' r' i:
Γ ⊢i (r ---> r') using i →
∀ l₁ l₂ g,
mkMLGoal Σ Γ (l₁ ++ (mkNH _ n' r')::l₂) g i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ n r)::l₂ ) g i.
Ltac2 do_mlApplyMetaRawIn (t : constr) (name : constr) :=
eapply cast_proof_ml_hyps;
f_equal;
run_in_reshaped_by_name name (fun () ⇒
eapply (@MLGoal_applyMetaIn _ _ _ _ $name _ _ $t)
)
.
Ltac do_mlApplyMetaRawIn t name :=
let f := ltac2:(t name |- do_mlApplyMetaRawIn (Option.get (Ltac1.to_constr t)) (Option.get (Ltac1.to_constr name))) in
f t name
.
Ltac2 do_mlApplyMetaRaw0 (t : constr) (cl : constr option) :=
match cl with
| None ⇒ do_mlApplyMetaRaw t
| Some n ⇒ do_mlApplyMetaRawIn t n
end
.
Ltac2 Notation "_mlApplyMetaRaw" t(constr) cl(opt(seq("in", constr))) :=
do_mlApplyMetaRaw0 t cl
.
Tactic Notation "mlApplyMetaRaw" constr(t) "in" constr(name) :=
let f := ltac2:(t name |- do_mlApplyMetaRawIn (Option.get (Ltac1.to_constr t)) (Option.get (Ltac1.to_constr name))) in
f t name
.
Local Example Private_ex_mlApplyMetaRawIn {Σ : Signature} Γ p q:
well_formed p →
well_formed q →
Γ ⊢i p ---> (p or q)
using BasicReasoning.
Ltac2 rec applyRec (f : constr) (xs : constr list) : constr option :=
match xs with
| [] ⇒ Some f
| y::ys ⇒
lazy_match! Constr.type f with
| (∀ _ : _, _) ⇒
Control.plus (fun () ⇒ applyRec constr:($f $y) ys) (fun _ ⇒ None)
| _ ⇒ None
end
end.
Ltac2 Eval (applyRec constr:(Nat.add) [constr:(1);constr:(2)]).
(*
All thic complicated code is here only for one reason:
I want to be able to first run the tactic with all the parameters
inferred or question marked, which results in another goal.
And then I want to handle the subgoals generated by the filling-in
underscores / question marks.
In particular, I want the proof mode goals to be generated first,
and the other, uninteresting goals, next.
*)
Ltac2 rec fillWithUnderscoresAndCall0
(tac : constr → unit) (t : constr) (args : constr list) :=
(*
Message.print (
Message.concat
(Message.of_string "fillWithUnderscoresAndCall: t = ")
(Message.of_constr t)
);
Message.print (
Message.concat
(Message.of_string "fillWithUnderscoresAndCall: args = ")
(List.fold_right (Message.concat) (Message.of_string "") (List.map Message.of_constr args))
);
*)
let cont := (fun () ⇒
lazy_match! Constr.type t with
| (?t' → ?_t's) ⇒ (* NOTE, (COQ BUG?) If I omit ?t's from here,
forall withh match this branch
NOTE2: This matching is fragile. Implication
hypotheses also seem to match the second branch
with forall _ : _ , _*)
lazy_match! goal with
| [|- ?g] ⇒
let h := Fresh.in_goal ident:(hasserted) in
assert($h : $t' → $g) > [(
let pftprime := Fresh.in_goal ident:(pftprime) in
intro $pftprime;
let new_t := open_constr:($t ltac2:(Notations.exact0 false (fun () ⇒ Control.hyp (pftprime)))) in
fillWithUnderscoresAndCall0 tac new_t args;
Std.clear [pftprime]
)|(
let h_constr := Control.hyp h in
apply $h_constr
)
]
end
| (∀ _ : _, _) ⇒ fillWithUnderscoresAndCall0 tac open_constr:($t _) args
| ?remainder ⇒ Control.throw (Invalid_argument (Some (Message.concat (Message.concat (Message.of_string "Remainder type: ") (Message.of_constr remainder)) (Message.concat (Message.of_string ", of term") (Message.of_constr t)))))
end
) in
match (applyRec t args) with
| None ⇒
(* Cannot apply t to args => continue *)
cont ()
| Some result ⇒
(* Can apply to to args, *)
lazy_match! Constr.type result with
| (∀ _ : _, _) ⇒
(* but result would still accept an argument => continue *)
cont ()
| _ ⇒
(* and nothing more can be applied to the result => we are done *)
tac result
end
end
.
Ltac2 rec fillWithUnderscoresAndCall
(tac : constr → unit) (twb : Std.constr_with_bindings) (args : constr list)
:=
let t := Fresh.in_goal ident:(t) in
Notations.specialize0 (fun () ⇒ twb) (Some (Std.IntroNaming (Std.IntroIdentifier t)));
let t_constr := Control.hyp t in
fillWithUnderscoresAndCall0 tac t_constr args;
clear $t
.
(*
We have this double-primed version because we want to be able
to feed it the proof before feeding it the ProofInfoLe.
*)
Lemma useGenericReasoning'' {Σ : Signature} (Γ : Theory) (ϕ : Pattern) i' i:
Γ ⊢i ϕ using i' →
(ProofInfoLe i' i) →
Γ ⊢i ϕ using i.
(* TODO: Create error messages for the following tactics *)
Ltac2 _callCompletedAndCast (twb : Std.constr_with_bindings) (tac : constr → unit) :=
let tac' := (fun (t' : constr) ⇒
let tcast := open_constr:(@useGenericReasoning'' _ _ _ _ _ $t') in
fillWithUnderscoresAndCall0 tac tcast []
) in
let t := Fresh.in_goal ident:(t) in
Notations.specialize0 (fun () ⇒ twb) (Some (Std.IntroNaming (Std.IntroIdentifier t)));
let t_constr := Control.hyp t in
fillWithUnderscoresAndCall0 tac' t_constr [];
clear $t
.
Ltac2 try_solve_pile_basic () :=
Control.enter (fun () ⇒
lazy_match! goal with
| [ |- (@ProofInfoLe _ _ _)] ⇒
try (solve
[ apply pile_any
| apply pile_refl
| apply pile_basic_generic
])
| [|- _] ⇒ ()
end
)
.
Ltac2 try_wfa () :=
Control.enter (fun () ⇒
let wfa := (fun p ⇒
if (Constr.has_evar p) then
()
else
ltac1:(try_wfauto2)
) in
lazy_match! goal with
| [|- well_formed ?p = true] ⇒ wfa p
| [|- is_true (well_formed ?p) ] ⇒ wfa p
| [|- Pattern.wf ?l = true] ⇒ wfa l
| [|- is_true (Pattern.wf ?l) ] ⇒ wfa l
| [|- _] ⇒ ()
end
)
.
Ltac2 mutable do_mlApplyMeta := fun (twb : Std.constr_with_bindings) ⇒
Control.enter (fun () ⇒
_ensureProofMode;
_callCompletedAndCast twb do_mlApplyMetaRaw ;
try_solve_pile_basic ();
try_wfa ()
)
.
Ltac2 mutable do_mlApplyMetaIn := fun (twb : Std.constr_with_bindings) (name : constr) ⇒
Control.enter (fun () ⇒
_ensureProofMode;
_callCompletedAndCast twb (fun t ⇒
do_mlApplyMetaRawIn t name
);
try_solve_pile_basic ();
try_wfa ()
)
.
Ltac2 do_mlApplyMeta0 (twb : Std.constr_with_bindings) (cl : constr option) :=
match cl with
| None ⇒ do_mlApplyMeta twb
| Some n ⇒ do_mlApplyMetaIn twb n
end
.
Ltac2 Notation "mlApplyMeta" t(seq(constr,with_bindings)) cl(opt(seq("in", constr))) :=
do_mlApplyMeta0 t cl
.
Ltac _mlApplyMeta t :=
let ff := ltac2:(t' |- do_mlApplyMeta ((Option.get (Ltac1.to_constr(t'))), Std.NoBindings)) in
ff t.
Ltac _mlApplyMetaIn t name :=
let ff := ltac2:(t' name' |- do_mlApplyMetaIn ((Option.get (Ltac1.to_constr(t')), Std.NoBindings)) (Option.get (Ltac1.to_constr(name')))) in
ff t name
.
Tactic Notation "mlApplyMeta" constr(t) :=
_mlApplyMeta t.
Tactic Notation "mlApplyMeta" constr(t) "in" constr(name) :=
_mlApplyMetaIn t name
.
Lemma MLGoal_destructAnd {Σ : Signature} Γ g l₁ l₂ nx x ny y nxy i:
mkMLGoal Σ Γ (l₁ ++ (mkNH _ nx x)::(mkNH _ ny y)::l₂ ) g i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ nxy (x and y))::l₂) g i.
Ltac2 mlDestructAnd_as (name : constr) (name1 : constr) (name2 : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
_failIfUsed $name1;
_failIfUsed $name2;
run_in_reshaped_by_name name (fun () ⇒
Control.plus(fun () ⇒
apply MLGoal_destructAnd with (nxy := $name) (nx := $name1) (ny := $name2)
)
(fun _ ⇒
_mlReshapeHypsBack;
throw_pm_exn_with_goal "mlDestructAnd_as: Given matching logic hypothesis is not a conjunction! ")
)
)
.
Ltac2 Notation "mlDestructAnd" name(constr) "as" name1(constr) name2(constr) :=
mlDestructAnd_as name name1 name2
.
Tactic Notation "mlDestructAnd" constr(name) "as" constr(name1) constr(name2) :=
let f := ltac2:(name name1 name2 |- mlDestructAnd_as (Option.get (Ltac1.to_constr name)) (Option.get (Ltac1.to_constr name1)) (Option.get (Ltac1.to_constr name2))) in
f name name1 name2
.
Ltac2 do_mlDestructAnd (name : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
let hyps := do_getHypNames () in
let name0 := eval cbv in (fresh $hyps) in
let name1 := eval cbv in (fresh ($name0 :: $hyps)) in
mlDestructAnd $name as $name0 $name1
)
.
Ltac2 Notation "mlDestructAnd" name(constr) :=
do_mlDestructAnd name
.
Tactic Notation "mlDestructAnd" constr(name) :=
let f := ltac2:(name |- do_mlDestructAnd (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example ex_mlDestructAnd {Σ : Signature} Γ a b p q:
well_formed a →
well_formed b →
well_formed p →
well_formed q →
Γ ⊢i p and q ---> a and b ---> q ---> a
using BasicReasoning.
Lemma and_of_equiv_is_equiv {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i (p <---> p') using i →
Γ ⊢i (q <---> q') using i →
Γ ⊢i ((p and q) <---> (p' and q')) using i.
Lemma or_of_equiv_is_equiv {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i (p <---> p') using i →
Γ ⊢i (q <---> q') using i →
Γ ⊢i ((p or q) <---> (p' or q')) using i.
Lemma impl_iff_notp_or_q {Σ : Signature} Γ p q:
well_formed p →
well_formed q →
Γ ⊢i ((p ---> q) <---> (! p or q))
using BasicReasoning.
Lemma p_and_notp_is_bot {Σ : Signature} Γ p:
well_formed p →
Γ ⊢i (⊥ <---> p and ! p)
using BasicReasoning.
Ltac2 do_mlExFalso ():=
_ensureProofMode;
mlApplyMeta bot_elim
.
Ltac2 Notation "mlExFalso"
:= do_mlExFalso ()
.
Ltac mlExFalso :=
ltac2:(do_mlExFalso ())
.
Ltac2 do_mlDestructBot (name' : constr) :=
Control.enter(fun () ⇒
run_in_reshaped_by_name name' (fun () ⇒
mlExFalso;
do_mlExact name'
)
)
.
Ltac2 Notation "mlDestructBot" name(constr) :=
do_mlDestructBot name
.
Tactic Notation "mlDestructBot" constr(name') :=
let f := ltac2:(name |- do_mlDestructBot (Option.get (Ltac1.to_constr name))) in
f name'
.
Lemma weird_lemma {Σ : Signature} Γ A B L R:
well_formed A →
well_formed B →
well_formed L →
well_formed R →
Γ ⊢i (((L and A) ---> (B or R)) ---> (L ---> ((A ---> B) or R)))
using BasicReasoning.
Lemma weird_lemma_meta {Σ : Signature} Γ A B L R i:
well_formed A →
well_formed B →
well_formed L →
well_formed R →
Γ ⊢i ((L and A) ---> (B or R)) using i →
Γ ⊢i (L ---> ((A ---> B) or R)) using i.
Lemma imp_trans_mixed_meta {Σ : Signature} Γ A B C D i :
well_formed A → well_formed B → well_formed C → well_formed D →
Γ ⊢i (C ---> A) using i →
Γ ⊢i (B ---> D) using i →
Γ ⊢i ((A ---> B) ---> C ---> D) using i.
Lemma and_weaken {Σ : Signature} A B C Γ i:
well_formed A → well_formed B → well_formed C →
Γ ⊢i (B ---> C) using i →
Γ ⊢i ((A and B) ---> (A and C)) using i.
Lemma impl_and {Σ : Signature} Γ A B C D i:
well_formed A → well_formed B → well_formed C → well_formed D →
Γ ⊢i (A ---> B) using i →
Γ ⊢i (C ---> D) using i →
Γ ⊢i (A and C) ---> (B and D) using i.
Lemma and_drop {Σ : Signature} A B C Γ i:
well_formed A → well_formed B → well_formed C →
Γ ⊢i ((A and B) ---> C) using i →
Γ ⊢i ((A and B) ---> (A and C)) using i.
Lemma prf_equiv_of_impl_of_equiv {Σ : Signature} Γ a b a' b' i:
well_formed a = true →
well_formed b = true →
well_formed a' = true →
well_formed b' = true →
Γ ⊢i (a <---> a') using i →
Γ ⊢i (b <---> b') using i →
Γ ⊢i (a ---> b) <---> (a' ---> b') using i.
Lemma lhs_to_and {Σ : Signature} Γ a b c i:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i (a and b) ---> c using i →
Γ ⊢i a ---> b ---> c using i.
Lemma lhs_from_and {Σ : Signature} Γ a b c i:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i a ---> b ---> c using i →
Γ ⊢i (a and b) ---> c using i.
Lemma prf_conj_split {Σ : Signature} Γ a b l:
well_formed a →
well_formed b →
Pattern.wf l →
Γ ⊢i (foldr patt_imp a l) ---> (foldr patt_imp b l) ---> (foldr patt_imp (a and b) l)
using BasicReasoning.
Lemma prf_conj_split_meta {Σ : Signature} Γ a b l (i : ProofInfo):
well_formed a →
well_formed b →
Pattern.wf l →
Γ ⊢i (foldr patt_imp a l) using i →
Γ ⊢i (foldr patt_imp b l) ---> (foldr patt_imp (a and b) l) using i.
Lemma prf_conj_split_meta_meta {Σ : Signature} Γ a b l (i : ProofInfo):
well_formed a →
well_formed b →
Pattern.wf l →
Γ ⊢i (foldr patt_imp a l) using i →
Γ ⊢i (foldr patt_imp b l) using i →
Γ ⊢i (foldr patt_imp (a and b) l) using i.
Lemma MLGoal_splitAnd {Σ : Signature} Γ a b l i:
mkMLGoal Σ Γ l a i →
mkMLGoal Σ Γ l b i →
mkMLGoal Σ Γ l (a and b) i.
Ltac2 do_mlSplitAnd () :=
Control.enter(fun () ⇒
_ensureProofMode;
Control.plus(fun () ⇒
apply MLGoal_splitAnd
)
(fun _ ⇒ throw_pm_exn_with_goal "do_mlSplitAnd: matching logic goal is not a conjunction! ")
)
.
Ltac2 Notation "mlSplitAnd" :=
do_mlSplitAnd ()
.
Ltac mlSplitAnd :=
ltac2:(do_mlSplitAnd ())
.
Local Lemma ex_mlSplitAnd {Σ : Signature} Γ a b c:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i a ---> b ---> c ---> (a and b)
using BasicReasoning.
Lemma prf_local_goals_equiv_impl_full_equiv {Σ : Signature} Γ g₁ g₂ l:
well_formed g₁ →
well_formed g₂ →
Pattern.wf l →
Γ ⊢i (foldr patt_imp (g₁ <---> g₂) l) --->
((foldr patt_imp g₁ l) <---> (foldr patt_imp g₂ l))
using BasicReasoning.
Lemma prf_local_goals_equiv_impl_full_equiv_meta {Σ : Signature} Γ g₁ g₂ l i:
well_formed g₁ →
well_formed g₂ →
Pattern.wf l →
Γ ⊢i (foldr patt_imp (g₁ <---> g₂) l) using i →
Γ ⊢i ((foldr patt_imp g₁ l) <---> (foldr patt_imp g₂ l)) using i.
Lemma prf_local_goals_equiv_impl_full_equiv_meta_proj1 {Σ : Signature} Γ g₁ g₂ l i:
well_formed g₁ →
well_formed g₂ →
Pattern.wf l →
Γ ⊢i (foldr patt_imp (g₁ <---> g₂) l) using i →
Γ ⊢i (foldr patt_imp g₁ l) using i →
Γ ⊢i (foldr patt_imp g₂ l) using i.
Lemma prf_local_goals_equiv_impl_full_equiv_meta_proj2 {Σ : Signature} Γ g₁ g₂ l i:
well_formed g₁ →
well_formed g₂ →
Pattern.wf l →
Γ ⊢i (foldr patt_imp (g₁ <---> g₂) l) using i →
Γ ⊢i (foldr patt_imp g₂ l) using i →
Γ ⊢i (foldr patt_imp g₁ l) using i.
Lemma top_holds {Σ : Signature} Γ:
Γ ⊢i Top using BasicReasoning.
Lemma phi_iff_phi_top {Σ : Signature} Γ ϕ :
well_formed ϕ →
Γ ⊢i ϕ <---> (ϕ <---> Top)
using BasicReasoning.
Lemma not_phi_iff_phi_bott {Σ : Signature} Γ ϕ :
well_formed ϕ →
Γ ⊢i (! ϕ ) <---> (ϕ <---> ⊥)
using BasicReasoning.
Lemma not_not_iff {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i A <---> ! ! A
using BasicReasoning.
Lemma patt_and_comm {Σ : Signature} Γ p q:
well_formed p →
well_formed q →
Γ ⊢i (p and q) <---> (q and p)
using BasicReasoning.
(* We need to come up with tactics that make this easier. *)
Local Example ex_mt {Σ : Signature} Γ ϕ₁ ϕ₂:
well_formed ϕ₁ →
well_formed ϕ₂ →
Γ ⊢i (! ϕ₁ ---> ! ϕ₂) ---> (ϕ₂ ---> ϕ₁)
using BasicReasoning.
Lemma lhs_and_to_imp {Σ : Signature} Γ (g x : Pattern) (xs : list Pattern):
well_formed g →
well_formed x →
Pattern.wf xs →
Γ ⊢i (foldr patt_and x xs ---> g) ---> (foldr patt_imp g (x :: xs))
using BasicReasoning.
Lemma lhs_and_to_imp_meta {Σ : Signature} Γ (g x : Pattern) (xs : list Pattern) i:
well_formed g →
well_formed x →
Pattern.wf xs →
Γ ⊢i (foldr patt_and x xs ---> g) using i →
Γ ⊢i (foldr patt_imp g (x :: xs)) using i.
Lemma lhs_imp_to_and {Σ : Signature} Γ (g x : Pattern) (xs : list Pattern):
well_formed g →
well_formed x →
Pattern.wf xs →
Γ ⊢i (foldr patt_imp g (x :: xs)) ---> (foldr patt_and x xs ---> g)
using BasicReasoning.
Lemma lhs_imp_to_and_meta {Σ : Signature} Γ (g x : Pattern) (xs : list Pattern) i:
well_formed g →
well_formed x →
Pattern.wf xs →
Γ ⊢i (foldr patt_imp g (x :: xs)) using i →
Γ ⊢i (foldr patt_and x xs ---> g) using i.
Lemma foldr_and_impl_last {Σ : Signature} Γ (x : Pattern) (xs : list Pattern):
well_formed x →
Pattern.wf xs →
Γ ⊢i (foldr patt_and x xs ---> x) using BasicReasoning.
Lemma foldr_and_weaken_last {Σ : Signature} Γ (x y : Pattern) (xs : list Pattern):
well_formed x →
well_formed y →
Pattern.wf xs →
Γ ⊢i (x ---> y) ---> (foldr patt_and x xs ---> foldr patt_and y xs) using BasicReasoning.
Lemma foldr_and_weaken_last_meta {Σ : Signature} Γ (x y : Pattern) (xs : list Pattern) i:
well_formed x →
well_formed y →
Pattern.wf xs →
Γ ⊢i (x ---> y) using i →
Γ ⊢i (foldr patt_and x xs ---> foldr patt_and y xs) using i.
Lemma foldr_and_last_rotate {Σ : Signature} Γ (x1 x2 : Pattern) (xs : list Pattern):
well_formed x1 →
well_formed x2 →
Pattern.wf xs →
Γ ⊢i ((foldr patt_and x2 (xs ++ [x1])) <---> (x2 and (foldr patt_and x1 xs))) using BasicReasoning.
Lemma foldr_and_last_rotate_1 {Σ : Signature} Γ (x1 x2 : Pattern) (xs : list Pattern):
well_formed x1 →
well_formed x2 →
Pattern.wf xs →
Γ ⊢i ((foldr patt_and x2 (xs ++ [x1])) ---> (x2 and (foldr patt_and x1 xs))) using BasicReasoning.
Lemma foldr_and_last_rotate_2 {Σ : Signature} Γ (x1 x2 : Pattern) (xs : list Pattern):
well_formed x1 →
well_formed x2 →
Pattern.wf xs →
Γ ⊢i ((x2 and (foldr patt_and x1 xs)) ---> ((foldr patt_and x2 (xs ++ [x1])))) using BasicReasoning.
#[local]
Ltac2 rec tryExact (l : constr) (idx : constr) :=
lazy_match! l with
| nil ⇒ throw_pm_exn_with_goal "tryExact: there was no matching logic hypothesis which is exactly matched by the goal: "
| (_ :: ?m) ⇒ Control.plus (fun () ⇒ do_mlExactn idx) (fun _ ⇒ tryExact m constr:($idx + 1))
end.
#[global]
Ltac2 do_mlAssumption () :=
Control.enter(fun () ⇒
_ensureProofMode;
lazy_match! goal with
| [ |- @of_MLGoal _ (@mkMLGoal _ _ ?l _ _) ]
⇒
tryExact l constr:(0)
end
)
.
Ltac2 Notation "mlAssumption" :=
do_mlAssumption ()
.
Tactic Notation "mlAssumption" :=
ltac2:(do_mlAssumption ())
.
Lemma impl_eq_or {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( (a ---> b) <---> ((! a) or b) )
using BasicReasoning.
Lemma nimpl_eq_and {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( ! (a ---> b) <---> (a and !b) )
using BasicReasoning.
Lemma deMorgan_nand_1 {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( !(a and b) ---> (!a or !b) )
using BasicReasoning.
Lemma deMorgan_nand_2 {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( (!a or !b) ---> !(a and b) )
using BasicReasoning.
Lemma deMorgan_nand {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( !(a and b) <---> (!a or !b) )
using BasicReasoning.
Lemma deMorgan_nor_1 {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( !(a or b) ---> (!a and !b))
using BasicReasoning.
Lemma deMorgan_nor_2 {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( (!a and !b) ---> !(a or b))
using BasicReasoning.
Lemma deMorgan_nor {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( !(a or b) <---> (!a and !b))
using BasicReasoning.
Lemma not_not_eq {Σ : Signature} (Γ : Theory) (a : Pattern) :
well_formed a →
Γ ⊢i (!(!a) <---> a)
using BasicReasoning.
Lemma and_singleton {Σ : Signature} : ∀ Γ p,
well_formed p → Γ ⊢i (p and p) <---> p using BasicReasoning.
Lemma bott_and {Σ : Signature} Γ ϕ :
well_formed ϕ →
Γ ⊢ ⊥ and ϕ <---> ⊥.
Lemma top_and {Σ : Signature} Γ ϕ :
well_formed ϕ →
Γ ⊢ Top and ϕ <---> ϕ.
Lemma MLGoal_ExactMeta {Σ:Signature} : ∀ Γ l g i,
Γ ⊢i g using i →
mkMLGoal Σ Γ l g i.
Tactic Notation "mlExactMeta" uconstr(t) :=
_ensureProofMode;
apply (@MLGoal_ExactMeta _ _ _ _ _ t).
Goal ∀ (Σ : Signature) Γ, Γ ⊢i Top using BasicReasoning.
Local Example exfalso_test {Σ : Signature} p Γ i :
well_formed p →
Γ ⊢i p and ! p ---> Top using i.
Local Example destruct_bot_test {Σ : Signature} p Γ i :
well_formed p →
Γ ⊢i ⊥ ---> Top using i.
Lemma extract_common_from_equivalence
{Σ : Signature} (Γ : Theory) (a b c : Pattern):
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i (((a and b) <---> (a and c)) <---> (a ---> (b <---> c)))
using BasicReasoning
.
Lemma extract_common_from_equivalence_1
{Σ : Signature} (Γ : Theory) (a b c : Pattern):
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i ((a ---> (b <---> c)) ---> ((a and b) <---> (a and c)))
using BasicReasoning
.
Lemma extract_common_from_equivalence_2
{Σ : Signature} (Γ : Theory) (a b c : Pattern):
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i (((a and b) <---> (a and c)) ---> (a ---> (b <---> c)))
using BasicReasoning
.
Ltac2 do_mlClassic_as (p : constr) (n1 : constr) (n2 : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
let hyps := do_getHypNames () in
let tmpName := eval cbv in (fresh $hyps) in
let wfName := Fresh.in_goal ident:(Hwf) in
lazy_match! goal with
| [|- @of_MLGoal _ (@mkMLGoal _ ?ctx ?_l ?_g ?i)]
⇒ assert ($wfName : well_formed $p = true)>
[()|(
let wf_hyp := Control.hyp wfName in
mlAdd (useBasicReasoning $i (A_or_notA $ctx $p $wf_hyp)) as $tmpName;
mlDestructOr $tmpName as $n1 $n2
)]
end
)
.
Ltac2 Notation "mlClassic" p(constr) "as" n1(constr) n2(constr) :=
do_mlClassic_as p n1 n2
.
Tactic Notation "mlClassic" constr(p) "as" constr(n1) constr(n2) :=
let f := ltac2:(p n1 n2 |- do_mlClassic_as (Option.get (Ltac1.to_constr p)) (Option.get (Ltac1.to_constr n1)) (Option.get (Ltac1.to_constr n2))) in
f p n1 n2
.
#[local]
Example exMlClassic {Σ : Signature} (Γ : Theory) (a : Pattern):
well_formed a →
Γ ⊢ (a or !a).
Lemma prf_clear_hyps_meta {Σ : Signature} Γ l1 l2 l3 g i:
Pattern.wf l1 →
Pattern.wf l2 →
Pattern.wf l3 →
well_formed g →
Γ ⊢i (foldr patt_imp g (l1 ++ l3)) using i →
Γ ⊢i (foldr patt_imp g (l1 ++ l2 ++ l3)) using i.
Lemma MLGoal_ApplyIn {Σ : Signature} Γ l1 l2 l3 name1 name2 h h' g i:
mkMLGoal Σ Γ (l1 ++ (mkNH _ name1 h') :: l2 ++ (mkNH _ name2 (h ---> h')) :: l3) g i →
mkMLGoal Σ Γ (l1 ++ (mkNH _ name1 h) :: l2 ++ (mkNH _ name2 (h ---> h')) :: l3) g i.
Lemma MLGoal_Swap {Σ : Signature} Γ l1 l2 l3 name1 name2 h1 h2 g i:
mkMLGoal Σ Γ (l1 ++ (mkNH _ name1 h1) :: l2 ++ (mkNH _ name2 h2) :: l3) g i →
mkMLGoal Σ Γ (l1 ++ (mkNH _ name2 h2) :: l2 ++ (mkNH _ name1 h1) :: l3) g i.
Ltac2 do_mlSwap (n1 : constr) (n2 : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
_mlReshapeHypsBy2Names n1 n2;
apply MLGoal_Swap;
_mlReshapeHypsBackTwice
)
.
Ltac2 Notation "mlSwap" n1(constr) "with" n2(constr) :=
do_mlSwap n1 n2.
Tactic Notation "mlSwap" constr(n1) "with" constr(n2) :=
let f := ltac2:(n1 n2 |- do_mlSwap (Option.get (Ltac1.to_constr n1)) (Option.get (Ltac1.to_constr n2))) in
f n1 n2.
Ltac2 do_mlApplyIn (name1' : constr) (name2' : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
_mlReshapeHypsBy2Names name1' name2';
(
(* Check the order of the hypotheses *)
match! goal with
| [ |- @of_MLGoal _ (@mkMLGoal _ _ (_ ++ ((@mkNH _ _ ?_h :: _) ++ (@mkNH _ _ (?_h ---> _) :: _))) _ _) ] ⇒
apply MLGoal_ApplyIn;
_mlReshapeHypsBackTwice
| [ |- _ ] ⇒ _mlReshapeHypsBackTwice;
mlSwap $name1' with $name2';
_mlReshapeHypsBy2Names name2' name1' ;
apply MLGoal_ApplyIn;
_mlReshapeHypsBackTwice;
mlSwap $name1' with $name2'
end
)
)
.
Ltac2 Notation "mlApply" n1(constr) "in" n2(constr) :=
do_mlApplyIn n1 n2.
Tactic Notation "mlApply" constr(name1') "in" constr(name2') :=
let f := ltac2:(name1' name2' |- do_mlApplyIn (Option.get (Ltac1.to_constr name1')) (Option.get (Ltac1.to_constr name2'))) in
f name1' name2'.
Example ex_mlApplyIn {Σ : Signature} Γ a b c d e f i:
well_formed a → well_formed b →
well_formed c → well_formed d →
well_formed e → well_formed f →
Γ ⊢i (c---> a ---> c ---> (a ---> b) ---> a ---> b) using i.
Lemma MLGoal_conjugate_hyps {Σ : Signature}
(Γ : Theory)
(l1 l2 l3 : hypotheses)
(name1 name2 conj_name : string)
(goal p1 p2 : Pattern)
(info : ProofInfo):
(* well_formed p1 -> well_formed p2 ->
Pattern.wf (map nh_patt (l1 ++ l2 ++ l3)) -> *)
mkMLGoal Σ Γ ((mkNH _ conj_name (p1 and p2)) :: (l1 ++ (mkNH _ name1 p1) :: l2 ++ (mkNH _ name2 p2) :: l3)) goal info →
mkMLGoal Σ Γ (l1 ++ (mkNH _ name1 p1) :: l2 ++ (mkNH _ name2 p2) :: l3) goal info.
Lemma patt_and_comm_basic {Σ : Signature}
(Γ : Theory)
(φ1 φ2 : Pattern) :
well_formed φ1 → well_formed φ2 →
Γ ⊢i φ1 and φ2 ---> φ2 and φ1 using BasicReasoning.
Ltac2 do_mlConj (n1 : constr) (n2 : constr) (conj_name' : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
do_failIfUsed conj_name';
_mlReshapeHypsBy2Names n1 n2;
apply MLGoal_conjugate_hyps with (conj_name := $conj_name');
rewrite app_comm_cons;
_mlReshapeHypsBackTwice;
lazy_match! goal with
| [ |- @of_MLGoal _ (@mkMLGoal _ _ ?l _ _) ] ⇒
lazy_match! eval cbv in (index_of $n1 (names_of $l)) with
| (Some ?i1) ⇒
lazy_match! eval cbv in (index_of $n2 (names_of $l)) with
| (Some ?i2) ⇒
lazy_match! (eval cbv in (Nat.compare $i1 $i2)) with
| (Lt) ⇒ ()
| (Gt) ⇒ mlApplyMeta patt_and_comm_basic in $conj_name'
| (Eq) ⇒ throw_pm_exn_with_goal "do_mlConj: Equal names were used"
end
| (None) ⇒ throw_pm_exn (Message.concat (Message.of_string "do_mlConj: No such name: ") (Message.of_constr n2))
end
| (None) ⇒ throw_pm_exn (Message.concat (Message.of_string "do_mlConj: No such name: ") (Message.of_constr n1))
end
end
).
Ltac2 Notation "mlConj" n1(constr) n2(constr) "as" n3(constr) :=
do_mlConj n1 n2 n3.
Tactic Notation "mlConj" constr(n1) constr(n2) "as" constr(n3) :=
let f := ltac2:(n1 n2 n3 |- do_mlConj (Option.get (Ltac1.to_constr n1)) (Option.get (Ltac1.to_constr n2)) (Option.get (Ltac1.to_constr n3))) in
f n1 n2 n3.
Ltac2 rec do_mlConj_many l (name : constr) : unit :=
match l with
| [] ⇒ throw_pm_exn (Message.of_string "do_mlConj_many: empty list")
| a :: t1 ⇒
match t1 with
| [] ⇒ throw_pm_exn (Message.of_string "do_mlConj_many: singleton list")
| b :: t2 ⇒
match t2 with
| [] ⇒ mlConj $a $b as $name
| _ :: _ ⇒
do_mlConj_many t1 name;
let hyps := do_getHypNames () in
let newname := eval cbv in (fresh $hyps) in
(* rename name into newname
TODO: optimise this with mlRename, which is independent of ML proofs: *)
mlRename $name into $newname;
mlConj $a $newname as $name;
mlClear $newname
end
end
end.
Ltac2 Notation "mlConj" l(list1(constr, ",")) "as" n3(constr) :=
do_mlConj_many l n3.
(**********************************************************************************)
Example ex_ml_conj_intro {Σ : Signature} Γ a b c d e f i:
well_formed a → well_formed b →
well_formed c → well_formed d →
well_formed e → well_formed f →
Γ ⊢i (a ---> b ---> c ---> d ---> e ---> f ---> (b and e)) using i.
Example ex_ml_conj_many_intro {Σ : Signature} Γ a b c d e f i:
well_formed a → well_formed b →
well_formed c → well_formed d →
well_formed e → well_formed f →
Γ ⊢i a ---> b ---> c ---> d ---> e ---> f ---> (a and (b and (c and e))) using i.
(* This is an example and belongs to the end of this file.
Its only purpose is only to show as many tactics as possible.\
*)
Example ex_and_of_equiv_is_equiv_2 {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i (p <---> p') using i →
Γ ⊢i (q <---> q') using i →
Γ ⊢i ((p and q) <---> (p' and q')) using i.
#[local]
Example ex_or_of_equiv_is_equiv_2 {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i (p <---> p') using i →
Γ ⊢i (q <---> q') using i →
Γ ⊢i ((p or q) <---> (p' or q')) using i.
Class MLReflexive {Σ : Signature} (op : Pattern → Pattern → Pattern) := {
reflexive_op_well_formed : ∀ φ ψ,
well_formed (op φ ψ) → well_formed φ ∧ well_formed ψ;
mlReflexivity :
∀ Γ φ i, well_formed φ → Γ ⊢i op φ φ using i;
}.
#[global]
Instance patt_imp_is_reflexive {Σ : Signature} : @MLReflexive Σ patt_imp.
#[export]
Hint Resolve patt_imp_is_reflexive : core.
#[global]
Instance patt_iff_is_reflexive {Σ : Signature} : @MLReflexive Σ patt_iff.
#[export]
Hint Resolve patt_iff_is_reflexive : core.
Lemma MLGoal_reflexivity {Σ : Signature} Γ l φ i op {_ : MLReflexive op} :
mkMLGoal _ Γ l (op φ φ) i.
Ltac2 do_mlReflexivity () :=
Control.enter(fun () ⇒
_ensureProofMode;
lazy_match! goal with
| [ |- @of_MLGoal _ (@mkMLGoal _ _ _ (?op ?_g ?_g) _) ] ⇒
match! goal with (* error handling *)
| [ |- _] ⇒ now (apply MLGoal_reflexivity; eauto)
| [ |- _] ⇒
throw_pm_exn
(Message.concat (Message.of_string "do_mlReflexivity: ")
(Message.concat (Message.of_constr op) (Message.of_string " is not reflexive!"))
)
end
| [ |- _] ⇒ Message.print (Message.of_string "Goal is not shaped as φ = φ!"); fail
end
).
Ltac2 Notation "mlReflexivity" :=
do_mlReflexivity ().
Tactic Notation "mlReflexivity" :=
ltac2:(do_mlReflexivity ()).
#[local]
Example reflexive_imp_test1 {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i p ---> p using i.
#[local]
Example notreflexive_and_test1 {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i p and p using i.
#[local]
Example reflexive_imp_test2 {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i q ---> q' ---> p' ---> p ---> p using i.
#[local]
Example reflexive_iff_test {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i q ---> q' ---> p' ---> p <---> p using i.
Lemma pf_iff_equiv_trans_obj {Σ : Signature} : ∀ Γ A B C i,
well_formed A → well_formed B → well_formed C →
Γ ⊢i (A <---> B) ---> (B <---> C) ---> (A <---> C) using i.
Lemma pf_iff_equiv_sym_obj {Σ : Signature} Γ A B i :
well_formed A → well_formed B → Γ ⊢i (A <---> B) ---> (B <---> A) using i.
(* TODO: make for other transitive relations too, then maybe move *)
Tactic Notation "mlTrans_iff" constr(b) :=
match goal with
| [ |- context[(mkMLGoal _ ?g ?h (patt_iff ?a ?c) ?i)] ] ⇒
let Htrans := fresh in
opose proof× (pf_iff_equiv_trans_obj g a b c i _ _ _) as Htrans;
last (
let Htrans2 := eval cbv in (fresh (map nh_name h)) in (
mlAssert (Htrans2 : (a <---> b));
last (
mlApplyMeta Htrans in Htrans2;
mlApply Htrans2;
mlClear Htrans2
)
);
last 2 [clear Htrans]
)
end.
Tactic Notation "emlTrans_iff" :=
let ep := fresh in
evar (ep : Pattern);
mlTrans_iff ep;
subst ep.
Lemma extract_common_from_equivalence_r {Σ : Signature} Γ a b c i :
well_formed a → well_formed b → well_formed c →
Γ ⊢i (b and a <---> c and a) <---> (a ---> b <---> c) using i.
Theorem provable_iff_top:
∀ {Σ : Signature} (Γ : Theory) (φ : Pattern) (i : ProofInfo),
well_formed φ →
Γ ⊢i φ using i →
Γ ⊢i φ <---> patt_top using i .
Theorem patt_and_id_r:
∀ {Σ : Signature} (Γ : Theory) (φ : Pattern),
well_formed φ →
Γ ⊢i φ and patt_top <---> φ using BasicReasoning .
From MatchingLogic Require Export BasicProofSystemLemmas.
From MatchingLogic.ProofMode Require Export Basics.
Import MatchingLogic.Logic.Notations.
Lemma MLGoal_exactn {Σ : Signature}
(Γ : Theory)
(l₁ l₂ : hypotheses)
(name : string)
(g : Pattern)
(info : ProofInfo) :
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name g) :: l₂) g info.
Ltac2 do_mlExactn (n : constr) :=
do_ensureProofMode ();
do_mlReshapeHypsByIdx n;
Control.plus (fun () ⇒ apply MLGoal_exactn)
(fun _ ⇒ _mlReshapeHypsBack;
throw_pm_exn_with_goal "do_mlExactn: Hypothesis is not identical to the goal!")
.
Ltac2 Notation "mlExactn" n(constr) :=
do_mlExactn n
.
Tactic Notation "mlExactn" constr(n) :=
let f := ltac2:(n |- do_mlExactn (Option.get (Ltac1.to_constr n))) in
f n
.
Lemma MLGoal_exact {Σ : Signature} Γ l name g idx info:
find_hyp name l = Some (idx, (mkNH _ name g)) →
mkMLGoal Σ Γ l g info.
Ltac2 do_mlExact (name' : constr) :=
do_ensureProofMode ();
Control.plus (fun () ⇒
eapply MLGoal_exact with (name := $name');
simpl; apply f_equal; reflexivity)
(fun _ ⇒ _mlReshapeHypsBack;
throw_pm_exn_with_goal ("do_mlExact: Given hypothesis is not identical to the goal, or there is no pattern associated with the given name!"))
.
Ltac2 Notation "mlExact" name(constr) :=
do_mlExact name
.
Tactic Notation "mlExact" constr(name) :=
let f := ltac2:(name |- do_mlExact (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example ex_mlExact {Σ : Signature} Γ a b c:
well_formed a = true →
well_formed b = true →
well_formed c = true →
Γ ⊢i a ---> b ---> c ---> b using BasicReasoning.
Lemma MLGoal_weakenConclusion' {Σ : Signature} Γ l g g' (i : ProofInfo):
Γ ⊢i g ---> g' using i →
mkMLGoal Σ Γ l g i →
mkMLGoal Σ Γ l g' i.
Lemma prf_contraction {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ((a ---> a ---> b) ---> (a ---> b)) using BasicReasoning.
Lemma prf_weaken_conclusion_under_implication {Σ : Signature} Γ a b c:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i ((a ---> b) ---> ((a ---> (b ---> c)) ---> (a ---> c))) using BasicReasoning.
Lemma prf_weaken_conclusion_under_implication_meta {Σ : Signature} Γ a b c (i : ProofInfo):
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i (a ---> b) using i →
Γ ⊢i ((a ---> (b ---> c)) ---> (a ---> c)) using i.
Lemma prf_weaken_conclusion_under_implication_meta_meta {Σ : Signature} Γ a b c i:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i a ---> b using i →
Γ ⊢i a ---> b ---> c using i →
Γ ⊢i a ---> c using i.
Lemma prf_weaken_conclusion_iter_under_implication {Σ : Signature} Γ l g g':
Pattern.wf l →
well_formed g →
well_formed g' →
Γ ⊢i (((g ---> g') ---> (foldr patt_imp g l)) ---> ((g ---> g') ---> (foldr patt_imp g' l)))
using BasicReasoning.
Lemma prf_weaken_conclusion_iter_under_implication_meta {Σ : Signature} Γ l g g' (i : ProofInfo):
Pattern.wf l →
well_formed g →
well_formed g' →
Γ ⊢i ((g ---> g') ---> (foldr patt_imp g l)) using i→
Γ ⊢i ((g ---> g') ---> (foldr patt_imp g' l)) using i.
Lemma MLGoal_weakenConclusion_under_first_implication {Σ : Signature} Γ l name g g' i:
mkMLGoal Σ Γ (mkNH _ name (g ---> g') :: l) g i →
mkMLGoal Σ Γ (mkNH _ name (g ---> g') :: l) g' i .
Lemma prf_weaken_conclusion_iter_under_implication_iter {Σ : Signature} Γ l₁ l₂ g g':
Pattern.wf l₁ →
Pattern.wf l₂ →
well_formed g →
well_formed g' →
Γ ⊢i ((foldr patt_imp g (l₁ ++ (g ---> g') :: l₂)) --->
(foldr patt_imp g' (l₁ ++ (g ---> g') :: l₂)))
using BasicReasoning.
Lemma prf_weaken_conclusion_iter_under_implication_iter_meta {Σ : Signature} Γ l₁ l₂ g g' i:
Pattern.wf l₁ →
Pattern.wf l₂ →
well_formed g →
well_formed g' →
Γ ⊢i (foldr patt_imp g (l₁ ++ (g ---> g') :: l₂)) using i →
Γ ⊢i (foldr patt_imp g' (l₁ ++ (g ---> g') :: l₂)) using i.
Lemma MLGoal_weakenConclusion {Σ : Signature} Γ l₁ l₂ name g g' i:
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name (g ---> g')) :: l₂) g i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name (g ---> g')) :: l₂) g' i.
Ltac2 run_in_reshaped_by_idx
(n : constr) (f : unit → unit) : unit :=
do_ensureProofMode ();
do_mlReshapeHypsByIdx n;
f ();
do_mlReshapeHypsBack ()
.
Ltac2 do_mlApplyn (n : constr) :=
run_in_reshaped_by_idx n ( fun () ⇒
Control.plus (fun () ⇒ apply MLGoal_weakenConclusion)
(fun _ ⇒ throw_pm_exn_with_goal "do_mlApplyn: Failed for goal: ")
)
.
Ltac2 Notation "mlApplyn" n(constr) :=
do_mlApplyn n
.
Tactic Notation "mlApplyn" constr(n) :=
let f := ltac2:(n |- do_mlApplyn (Option.get (Ltac1.to_constr n))) in
f n
.
Ltac2 run_in_reshaped_by_name
(name : constr) (f : unit → unit) : unit :=
do_ensureProofMode ();
do_mlReshapeHypsByName name;
f ();
do_mlReshapeHypsBack ()
.
Ltac2 do_mlApply (name' : constr) :=
run_in_reshaped_by_name name' (fun () ⇒
Control.plus (fun () ⇒ apply MLGoal_weakenConclusion)
(fun _ ⇒ throw_pm_exn_with_goal "do_mlApply: Goal does not match the conclusion of the hypothesis")
)
.
Ltac2 Notation "mlApply" name(constr) :=
do_mlApply name
.
Tactic Notation "mlApply" constr(name') :=
let f := ltac2:(name' |- do_mlApply (Option.get (Ltac1.to_constr name'))) in
f name'
.
Local Example ex_mlApplyn {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i a ---> (a ---> b) ---> b using BasicReasoning.
Lemma Constructive_dilemma {Σ : Signature} Γ p q r s:
well_formed p →
well_formed q →
well_formed r →
well_formed s →
Γ ⊢i ((p ---> q) ---> (r ---> s) ---> (p or r) ---> (q or s)) using BasicReasoning.
Lemma prf_impl_distr_meta {Σ : Signature} Γ a b c i:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i (a ---> (b ---> c)) using i →
Γ ⊢i ((a ---> b) ---> (a ---> c)) using i.
Lemma prf_add_lemma_under_implication {Σ : Signature} Γ l g h:
Pattern.wf l →
well_formed g →
well_formed h →
Γ ⊢i ((foldr patt_imp h l) --->
((foldr patt_imp g (l ++ [h])) --->
(foldr patt_imp g l)))
using BasicReasoning.
Lemma prf_add_lemma_under_implication_meta {Σ : Signature} Γ l g h i:
Pattern.wf l →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp h l) using i →
Γ ⊢i ((foldr patt_imp g (l ++ [h])) ---> (foldr patt_imp g l)) using i.
Lemma prf_add_lemma_under_implication_meta_meta {Σ : Signature} Γ l g h i:
Pattern.wf l →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp h l) using i →
Γ ⊢i (foldr patt_imp g (l ++ [h])) using i →
Γ ⊢i (foldr patt_imp g l) using i.
Lemma mlGoal_assert {Σ : Signature} Γ l name g h i:
well_formed h →
mkMLGoal Σ Γ l h i →
mkMLGoal Σ Γ (l ++ [mkNH _ name h]) g i →
mkMLGoal Σ Γ l g i.
Lemma impl_elim
{Σ: Signature}
(Γ : Theory)
(A B C : Pattern)
(l1 l2 : list Pattern)
(i : ProofInfo)
:
Γ ⊢i foldr patt_imp A (l1 ++ l2) using i →
Γ ⊢i foldr patt_imp C (l1 ++ B :: l2) using i →
Γ ⊢i foldr patt_imp C (l1 ++ (A ---> B)::l2) using i
.
Lemma mlGoal_destructImp {Σ : Signature} Γ l1 l2 name C A B i:
mkMLGoal Σ Γ (l1 ++ l2) A i →
mkMLGoal Σ Γ (l1 ++ (mkNH _ name B)::l2) C i →
mkMLGoal Σ Γ (l1 ++ (mkNH _ name (A ---> B))::l2) C i.
Ltac2 do_mlDestructImp (name : constr) :=
run_in_reshaped_by_name name (fun () ⇒
Control.plus (fun () ⇒ apply (mlGoal_destructImp _ _ _ $name))
(fun _ ⇒ throw_pm_exn_with_goal "do_mlDestructImp: The given hypothesis was not an implication pattern: ")
)
.
Ltac2 Notation "mlDestructImp" name(constr) :=
do_mlDestructImp name
.
Tactic Notation "mlDestructImp" constr(name) :=
let f := ltac2:(name |- do_mlDestructImp (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example Test_destructImp {Σ : Signature} Γ :
∀ A B C, well_formed A → well_formed B → well_formed C →
Γ ⊢i (A ---> B) ---> (B ---> C) ---> A ---> C using BasicReasoning.
Lemma MLGoal_revert {Σ : Signature} (Γ : Theory) (l1 l2 : hypotheses) (x g : Pattern) (n : string) i :
mkMLGoal Σ Γ (l1 ++ l2) (x ---> g) i →
mkMLGoal Σ Γ (l1 ++ (mkNH _ n x) :: l2) g i.
Ltac2 do_mlRevert (name : constr) :=
run_in_reshaped_by_name name (fun () ⇒
Control.plus (fun () ⇒ apply (MLGoal_revert _ _ _ _ _ $name))
(fun _ ⇒ throw_pm_exn_with_goal "do_mlRevert: failed for goal: ")
)
.
Ltac2 Notation "mlRevert" name(constr) :=
do_mlRevert name
.
Tactic Notation "mlRevert" constr(name) :=
let f := ltac2:(name |- do_mlRevert (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example Test_revert {Σ : Signature} Γ :
∀ A B C, well_formed A → well_formed B → well_formed C →
Γ ⊢i A ---> B ---> C ---> A using BasicReasoning.
Lemma prf_add_lemma_under_implication_generalized {Σ : Signature} Γ l1 l2 g h:
Pattern.wf l1 →
Pattern.wf l2 →
well_formed g →
well_formed h →
Γ ⊢i ((foldr patt_imp h l1) ---> ((foldr patt_imp g (l1 ++ [h] ++ l2)) ---> (foldr patt_imp g (l1 ++ l2))))
using BasicReasoning.
Lemma prf_add_lemma_under_implication_generalized_meta {Σ : Signature} Γ l1 l2 g h i:
Pattern.wf l1 →
Pattern.wf l2 →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp h l1) using i →
Γ ⊢i ((foldr patt_imp g (l1 ++ [h] ++ l2)) ---> (foldr patt_imp g (l1 ++ l2))) using i.
Lemma prf_add_lemma_under_implication_generalized_meta_meta {Σ : Signature} Γ l1 l2 g h i:
Pattern.wf l1 →
Pattern.wf l2 →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp h l1) using i →
Γ ⊢i (foldr patt_imp g (l1 ++ [h] ++ l2)) using i →
Γ ⊢i (foldr patt_imp g (l1 ++ l2)) using i.
Lemma mlGoal_assert_generalized {Σ : Signature} Γ l1 l2 name g h i:
well_formed h →
mkMLGoal Σ Γ l1 h i →
mkMLGoal Σ Γ (l1 ++ [mkNH _ name h] ++ l2) g i →
mkMLGoal Σ Γ (l1 ++ l2) g i.
Ltac2 do_mlAssert_nocheck
(name : constr) (t : constr) :=
lazy_match! goal with
| [ |- @of_MLGoal _ (@mkMLGoal ?sgm ?ctx ?l ?g ?i)] ⇒
let hwf := Fresh.in_goal ident:(Hwf) in
assert ($hwf : well_formed $t = true) >
[()|(
let hwf_constr := Control.hyp hwf in
let h := Fresh.in_goal ident:(H) in
assert ($h : @of_MLGoal $sgm (@mkMLGoal $sgm $ctx $l $t $i)) >
[() |
let h_constr := Control.hyp h in
(eapply (@mlGoal_assert $sgm $ctx $l $name $g $t $i $hwf_constr $h_constr);
ltac1:(rewrite [_ ++ _]/=); clear $h)]
)]
end.
Ltac2 Notation "_mlAssert_nocheck" "(" name(constr) ":" t(constr) ")" :=
do_mlAssert_nocheck name t
.
Tactic Notation "_mlAssert_nocheck" "(" constr(name) ":" constr(t) ")" :=
let f := ltac2:(name t |- do_mlAssert_nocheck (Option.get (Ltac1.to_constr name)) (Option.get (Ltac1.to_constr t))) in
f name t
.
Ltac2 do_mlAssert (name : constr) (t : constr) :=
do_ensureProofMode ();
do_failIfUsed name;
do_mlAssert_nocheck name t
.
Ltac2 Notation "mlAssert" "(" name(constr) ":" t(constr) ")" :=
do_mlAssert name t
.
(* TODO: make this bind tigther. *)
Tactic Notation "mlAssert" "(" constr(name) ":" constr(t) ")" :=
let f := ltac2:(name t |- do_mlAssert (Option.get (Ltac1.to_constr name)) (Option.get (Ltac1.to_constr t))) in
f name t
.
Ltac2 do_mlAssert_autonamed (t : constr) :=
do_ensureProofMode ();
let hyps := do_getHypNames () in
let name := eval lazy in (fresh $hyps) in
do_mlAssert name t
.
Ltac2 Notation "mlAssert" "(" t(constr) ")" :=
do_mlAssert_autonamed t
.
Tactic Notation "mlAssert" "(" constr(t) ")" :=
let f := ltac2:(t |- do_mlAssert_autonamed (Option.get (Ltac1.to_constr t))) in
f t
.
Local Example ex_mlAssert {Σ : Signature} Γ a:
well_formed a →
Γ ⊢i (a ---> a ---> a) using BasicReasoning.
Ltac2 _getGoalProofInfo () : constr :=
lazy_match! goal with
| [|- @of_MLGoal _ (@mkMLGoal _ _ _ _ ?i)]
⇒ i
end.
Ltac2 _getGoalTheory () : constr :=
lazy_match! goal with
| [|- @of_MLGoal _ (@mkMLGoal _ ?ctx _ _ _)]
⇒ ctx
end.
Ltac2 mlAssert_using_first
(name : constr) (t : constr) (n : constr) :=
do_ensureProofMode ();
do_failIfUsed name;
lazy_match! goal with
| [|- @of_MLGoal ?sgm (@mkMLGoal ?sgm ?ctx ?l ?g ?i)] ⇒
let l1 := Fresh.in_goal ident:(l1) in
let l2 := Fresh.in_goal ident:(l2) in
let heql1 := Fresh.in_goal ident:(Heql1) in
let heql2 := Fresh.in_goal ident:(Heql2) in
remember (take $n $l) as l1 eqn:$heql1 in |-;
remember (drop $n $l) as l2 eqn:$heql2 in |-;
simpl in Heql1; simpl in Heql2;
eapply cast_proof_ml_hyps >
[(
ltac1:(l n |- rewrite -[l](take_drop n)) (Ltac1.of_constr l) (Ltac1.of_constr n);
reflexivity
)|()];
let hwf := Fresh.in_goal ident:(Hwf) in
assert ($hwf : well_formed $t = true) >
[()|
let h := Fresh.in_goal ident:(H) in
let l1_constr := Control.hyp l1 in
(* let l2_constr := Control.hyp l2 in *)
let heql1_constr := Control.hyp heql1 in
let hwf_constr := Control.hyp hwf in
assert ($h : @of_MLGoal $sgm (@mkMLGoal $sgm $ctx $l1_constr $t $i)) >
[
(eapply cast_proof_ml_hyps>
[(rewrite → $heql1_constr; reflexivity)|()]);
clear $l1 $l2 $heql1 $heql2
|
let h_constr := Control.hyp h in
apply (cast_proof_ml_hyps _ _ _ (f_equal patterns_of $heql1_constr)) in $h;
eapply (@mlGoal_assert_generalized $sgm $ctx (take $n $l) (drop $n $l) $name $g $t $i $hwf_constr $h_constr);
ltac1:(rewrite [_ ++ _]/=);
clear $l1 $l2 $heql1 $heql2 $h
]
]
end.
Ltac2 Notation "mlAssert" "(" name(constr) ":" t(constr) ")" "using" "first" n(constr) :=
mlAssert_using_first name t n
.
Tactic Notation "mlAssert" "(" constr(name) ":" constr(t) ")" "using" "first" constr(n) :=
let f := ltac2:(name t n |- mlAssert_using_first (Option.get (Ltac1.to_constr name)) (Option.get (Ltac1.to_constr t)) (Option.get (Ltac1.to_constr n))) in
f name t n
.
Ltac2 mlAssert_autonamed_using_first
(t : constr) (n : constr) :=
do_ensureProofMode ();
let hyps := do_getHypNames () in
let name := eval cbv in (fresh $hyps) in
mlAssert_using_first name t n
.
Ltac2 Notation "mlAssert" "(" t(constr) ")" "using" "first" n(constr) :=
mlAssert_autonamed_using_first t n
.
Tactic Notation "mlAssert" "(" constr(t) ")" "using" "first" constr(n) :=
let f := ltac2:(t n |- mlAssert_autonamed_using_first (Option.get (Ltac1.to_constr t)) (Option.get (Ltac1.to_constr n))) in
f t n
.
Local Example ex_assert_using {Σ : Signature} Γ p q a b:
well_formed a = true →
well_formed b = true →
well_formed p = true →
well_formed q = true →
Γ ⊢i a ---> p and q ---> b ---> ! ! q using BasicReasoning.
Lemma P4i' {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i ((!A ---> A) ---> A) using BasicReasoning.
Lemma tofold {Σ : Signature} p:
p = fold_right patt_imp p [].
Lemma consume {Σ : Signature} p q l:
fold_right patt_imp (p ---> q) l = fold_right patt_imp q (l ++ [p]).
Lemma prf_disj_elim {Σ : Signature} Γ p q r:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i ((p ---> r) ---> (q ---> r) ---> (p or q) ---> r)
using BasicReasoning.
Lemma prf_disj_elim_meta {Σ : Signature} Γ p q r i:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i (p ---> r) using i →
Γ ⊢i ((q ---> r) ---> (p or q) ---> r) using i.
Lemma prf_disj_elim_meta_meta {Σ : Signature} Γ p q r i:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i (p ---> r) using i →
Γ ⊢i (q ---> r) using i →
Γ ⊢i ((p or q) ---> r) using i.
Lemma prf_disj_elim_meta_meta_meta {Σ : Signature} Γ p q r i:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i (p ---> r) using i →
Γ ⊢i (q ---> r) using i →
Γ ⊢i (p or q) using i →
Γ ⊢i r using i.
Lemma prf_add_proved_to_assumptions {Σ : Signature} Γ l a g i:
Pattern.wf l →
well_formed a →
well_formed g →
Γ ⊢i a using i→
Γ ⊢i ((foldr patt_imp g (a::l)) ---> (foldr patt_imp g l)) using i.
Lemma prf_add_proved_to_assumptions_meta {Σ : Signature} Γ l a g i:
Pattern.wf l →
well_formed a →
well_formed g →
Γ ⊢i a using i →
Γ ⊢i (foldr patt_imp g (a::l)) using i →
Γ ⊢i (foldr patt_imp g l) using i.
Lemma MLGoal_add {Σ : Signature} Γ l name g h i:
Γ ⊢i h using i →
mkMLGoal Σ Γ (mkNH _ name h::l) g i →
mkMLGoal Σ Γ l g i.
Ltac2 do_mlAdd_as (n : constr) (name' : constr) :=
do_ensureProofMode ();
do_failIfUsed name';
lazy_match! goal with
| [|- @of_MLGoal ?sgm (@mkMLGoal ?sgm ?ctx ?l ?g ?i)] ⇒
Control.plus(fun () ⇒
apply (@MLGoal_add $sgm $ctx $l $name' $g _ $i $n)
)
(fun _ ⇒ throw_pm_exn (Message.concat (Message.of_string "do_mlAdd_as: given Coq hypothesis is not a pattern: ") (Message.of_constr n)))
end.
Ltac2 Notation "mlAdd" n(constr) "as" name(constr) :=
do_mlAdd_as n name
.
Tactic Notation "mlAdd" constr(n) "as" constr(name') :=
let f := ltac2:(n name |- do_mlAdd_as (Option.get (Ltac1.to_constr n)) (Option.get (Ltac1.to_constr name))) in
f n name'
.
Ltac2 get_fresh_name () : constr :=
do_ensureProofMode ();
let hyps := do_getHypNames () in
let name := eval cbv in (fresh $hyps) in
name
.
Ltac2 do_mlAdd (n : constr) :=
do_mlAdd_as n (get_fresh_name ())
.
Ltac2 Notation "mlAdd" n(constr) :=
do_mlAdd n
.
Tactic Notation "mlAdd" constr(n) :=
let f := ltac2:(n |- do_mlAdd (Option.get (Ltac1.to_constr n))) in
f n
.
Local Example ex_mlAdd {Σ : Signature} Γ l g h i:
Pattern.wf l →
well_formed g →
well_formed h →
Γ ⊢i (h ---> g) using i →
Γ ⊢i h using i →
Γ ⊢i g using i.
Lemma prf_clear_hyp {Σ : Signature} Γ l1 l2 g h:
Pattern.wf l1 →
Pattern.wf l2 →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp g (l1 ++ l2)) ---> (foldr patt_imp g (l1 ++ [h] ++ l2))
using BasicReasoning.
Lemma prf_clear_hyp_meta {Σ : Signature} Γ l1 l2 g h i:
Pattern.wf l1 →
Pattern.wf l2 →
well_formed g →
well_formed h →
Γ ⊢i (foldr patt_imp g (l1 ++ l2)) using i →
Γ ⊢i (foldr patt_imp g (l1 ++ [h] ++ l2)) using i.
Lemma mlGoal_clear_hyp {Σ : Signature} Γ l1 l2 g h i:
mkMLGoal Σ Γ (l1 ++ l2) g i →
mkMLGoal Σ Γ (l1 ++ h::l2) g i.
Ltac2 do_mlClear (name : constr) :=
run_in_reshaped_by_name name (fun () ⇒
apply mlGoal_clear_hyp
)
.
Ltac2 Notation "mlClear" name(constr) :=
do_mlClear name
.
Tactic Notation "mlClear" constr(name) :=
let f := ltac2:(name |- do_mlClear (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example ex_mlClear {Σ : Signature} Γ a b c:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i a ---> (b ---> (c ---> b)) using BasicReasoning.
Lemma not_concl {Σ : Signature} Γ p q:
well_formed p →
well_formed q →
Γ ⊢i (p ---> (q ---> ((p ---> ! q) ---> ⊥))) using BasicReasoning.
Lemma reorder_last_to_head {Σ : Signature} Γ g x l:
Pattern.wf l →
well_formed g →
well_formed x →
Γ ⊢i ((foldr patt_imp g (x::l)) ---> (foldr patt_imp g (l ++ [x]))) using BasicReasoning.
Lemma reorder_last_to_head_meta {Σ : Signature} Γ g x l i:
Pattern.wf l →
well_formed g →
well_formed x →
Γ ⊢i (foldr patt_imp g (x::l)) using i →
Γ ⊢i (foldr patt_imp g (l ++ [x])) using i.
(* Iterated modus ponens.
For l = x₁, ..., xₙ, it says that
Γ ⊢i ((x₁ -> ... -> xₙ -> (x₁ -> ... -> xₙ -> r)) -> r)
*)
Lemma modus_ponens_iter {Σ : Signature} Γ l r:
Pattern.wf l →
well_formed r →
Γ ⊢i (foldr patt_imp r (l ++ [foldr patt_imp r l])) using BasicReasoning.
Lemma and_impl {Σ : Signature} Γ p q r:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i ((p and q ---> r) ---> (p ---> (q ---> r))) using BasicReasoning.
Lemma and_impl' {Σ : Signature} Γ p q r:
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i ((p ---> (q ---> r)) ---> ((p and q) ---> r)) using BasicReasoning.
Lemma prf_disj_elim_iter {Σ : Signature} Γ l p q r:
Pattern.wf l →
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i ((fold_right patt_imp r (l ++ [p]))
--->
((fold_right patt_imp r (l ++ [q]))
--->
(fold_right patt_imp r (l ++ [p or q]))))
using BasicReasoning.
Lemma prf_disj_elim_iter_2 {Σ : Signature} Γ l₁ l₂ p q r:
Pattern.wf l₁ →
Pattern.wf l₂ →
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i ((fold_right patt_imp r (l₁ ++ [p] ++ l₂))
--->
((fold_right patt_imp r (l₁ ++ [q] ++ l₂))
--->
(fold_right patt_imp r (l₁ ++ [p or q] ++ l₂))))
using BasicReasoning.
Lemma prf_disj_elim_iter_2_meta {Σ : Signature} Γ l₁ l₂ p q r i:
Pattern.wf l₁ →
Pattern.wf l₂ →
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i (fold_right patt_imp r (l₁ ++ [p] ++ l₂)) using i →
Γ ⊢i ((fold_right patt_imp r (l₁ ++ [q] ++ l₂))
--->
(fold_right patt_imp r (l₁ ++ [p or q] ++ l₂))) using i.
Lemma prf_disj_elim_iter_2_meta_meta {Σ : Signature} Γ l₁ l₂ p q r i:
Pattern.wf l₁ →
Pattern.wf l₂ →
well_formed p →
well_formed q →
well_formed r →
Γ ⊢i (fold_right patt_imp r (l₁ ++ [p] ++ l₂)) using i →
Γ ⊢i (fold_right patt_imp r (l₁ ++ [q] ++ l₂)) using i →
Γ ⊢i (fold_right patt_imp r (l₁ ++ [p or q] ++ l₂)) using i.
Lemma MLGoal_disj_elim {Σ : Signature} Γ l₁ l₂ pn p qn q pqn r i:
mkMLGoal Σ Γ (l₁ ++ (mkNH _ pn p) :: l₂) r i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ qn q) :: l₂) r i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ pqn (p or q)) :: l₂) r i.
Ltac2 do_mlDestructOr_as (name : constr) (name1 : constr) (name2 : constr) :=
do_ensureProofMode ();
do_failIfUsed name1;
do_failIfUsed name2;
lazy_match! goal with
| [|- @of_MLGoal _ (@mkMLGoal _ _ _ _ _)] ⇒
(* let htd := Fresh.in_goal ident:(Htd) in *)
eapply cast_proof_ml_hyps;
f_equal;
_mlReshapeHypsByName name;
Control.plus (fun () ⇒
apply MLGoal_disj_elim with (pqn := $name) (pn := $name1) (qn := $name2);
_mlReshapeHypsBack
)
(fun _ ⇒ _mlReshapeHypsBack;
throw_pm_exn_with_goal "do_mlDestructOr_as: failed for goal: ")
end
.
Ltac2 Notation "mlDestructOr" name(constr) "as" name1(constr) name2(constr) :=
do_mlDestructOr_as name name1 name2
.
Tactic Notation "mlDestructOr" constr(name) "as" constr(name1) constr(name2) :=
let f := ltac2:(name name1 name2 |- do_mlDestructOr_as (Option.get (Ltac1.to_constr name)) (Option.get (Ltac1.to_constr name1)) (Option.get (Ltac1.to_constr name2))) in
f name name1 name2
.
Ltac2 do_mlDestructOr (name : constr) :=
do_ensureProofMode ();
let hyps := do_getHypNames () in
let name0 := eval cbv in (fresh $hyps) in
let name1 := eval cbv in (fresh ($name0 :: $hyps)) in
mlDestructOr $name as $name0 $name1
.
Ltac2 Notation "mlDestructOr" name(constr) :=
do_mlDestructOr name
.
Tactic Notation "mlDestructOr" constr(name) :=
let f := ltac2:(name |- do_mlDestructOr (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example exd {Σ : Signature} Γ a b p q c i:
well_formed a →
well_formed b →
well_formed p →
well_formed q →
well_formed c →
Γ ⊢i (a ---> p ---> b ---> c) using i →
Γ ⊢i (a ---> q ---> b ---> c) using i→
Γ ⊢i (a ---> (p or q) ---> b ---> c) using i.
Lemma pf_iff_split {Σ : Signature} Γ A B i:
well_formed A →
well_formed B →
Γ ⊢i A ---> B using i →
Γ ⊢i B ---> A using i →
Γ ⊢i A <---> B using i.
Lemma pf_iff_proj1 {Σ : Signature} Γ A B i:
well_formed A →
well_formed B →
Γ ⊢i A <---> B using i →
Γ ⊢i A ---> B using i.
Lemma pf_iff_proj2 {Σ : Signature} Γ A B i:
well_formed A →
well_formed B →
Γ ⊢i (A <---> B) using i →
Γ ⊢i (B ---> A) using i.
Lemma pf_iff_iff {Σ : Signature} Γ A B i:
well_formed A →
well_formed B →
prod ((Γ ⊢i (A <---> B) using i) → (prod (Γ ⊢i (A ---> B) using i) (Γ ⊢i (B ---> A) using i)))
( (prod (Γ ⊢i (A ---> B) using i) (Γ ⊢i (B ---> A) using i)) → (Γ ⊢i (A <---> B) using i)).
Lemma pf_iff_equiv_refl {Σ : Signature} Γ A :
well_formed A →
Γ ⊢i (A <---> A) using BasicReasoning.
Lemma pf_iff_equiv_sym {Σ : Signature} Γ A B i:
well_formed A →
well_formed B →
Γ ⊢i (A <---> B) using i →
Γ ⊢i (B <---> A) using i.
Lemma pf_iff_equiv_trans {Σ : Signature} Γ A B C i:
well_formed A →
well_formed B →
well_formed C →
Γ ⊢i (A <---> B) using i →
Γ ⊢i (B <---> C) using i →
Γ ⊢i (A <---> C) using i.
Lemma prf_conclusion {Σ : Signature} Γ a b i:
well_formed a →
well_formed b →
Γ ⊢i b using i →
Γ ⊢i (a ---> b) using i.
Lemma and_of_negated_iff_not_impl {Σ : Signature} Γ p1 p2:
well_formed p1 →
well_formed p2 →
Γ ⊢i (! (! p1 ---> p2) <---> ! p1 and ! p2)
using BasicReasoning.
Lemma and_impl_2 {Σ : Signature} Γ p1 p2:
well_formed p1 →
well_formed p2 →
Γ ⊢i (! (p1 ---> p2) <---> p1 and ! p2)
using BasicReasoning.
Lemma conj_intro_meta_partial {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A → well_formed B →
Γ ⊢i A using i →
Γ ⊢i B ---> (A and B) using i.
Lemma and_impl_patt {Σ : Signature} (A B C : Pattern) Γ (i : ProofInfo):
well_formed A → well_formed B → well_formed C →
Γ ⊢i A using i →
Γ ⊢i ((A and B) ---> C) using i →
Γ ⊢i (B ---> C) using i.
Lemma conj_intro2 {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A → well_formed B →
Γ ⊢i (A ---> (B ---> (B and A)))
using BasicReasoning.
Lemma conj_intro_meta_partial2 {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo):
well_formed A → well_formed B →
Γ ⊢i A using i →
Γ ⊢i B ---> (B and A) using i.
Lemma and_impl_patt2 {Σ : Signature} (A B C : Pattern) Γ (i : ProofInfo):
well_formed A → well_formed B → well_formed C →
Γ ⊢i A using i →
Γ ⊢i ((B and A) ---> C) using i →
Γ ⊢i (B ---> C) using i.
Lemma patt_and_comm_meta {Σ : Signature} (A B : Pattern) (Γ : Theory) (i : ProofInfo) :
well_formed A → well_formed B
→
Γ ⊢i A and B using i →
Γ ⊢i B and A using i.
Lemma MLGoal_applyMeta {Σ : Signature} Γ r r' i:
Γ ⊢i (r' ---> r) using i →
∀ l,
mkMLGoal Σ Γ l r' i →
mkMLGoal Σ Γ l r i.
(* Error message of this one is sufficient *)
Ltac2 do_mlApplyMetaRaw (t : constr) :=
eapply (@MLGoal_applyMeta _ _ _ _ _ $t)
.
Ltac2 Notation "_mlApplyMetaRaw" t(open_constr) :=
do_mlApplyMetaRaw t
.
Tactic Notation "_mlApplyMetaRaw" uconstr(t) :=
let f := ltac2:(t |- do_mlApplyMetaRaw (Option.get (Ltac1.to_constr t))) in
f t
.
Lemma MLGoal_left {Σ : Signature} Γ l x y i:
mkMLGoal Σ Γ l x i →
mkMLGoal Σ Γ l (patt_or x y) i.
Lemma MLGoal_right {Σ : Signature} Γ l x y i:
mkMLGoal Σ Γ l y i →
mkMLGoal Σ Γ l (patt_or x y) i.
Ltac2 mlLeft () :=
_ensureProofMode;
Control.plus(fun () ⇒
apply MLGoal_left
)
(fun _ ⇒ throw_pm_exn_with_goal "mlLeft: Current matching logic goal is not a disjunction! ")
.
Ltac2 mlRight () :=
_ensureProofMode;
Control.plus(fun () ⇒
apply MLGoal_right
)
(fun _ ⇒ throw_pm_exn_with_goal "mlLeft: Current matching logic goal is not a disjunction! ")
.
Ltac mlLeft := ltac2:(mlLeft ()).
Ltac mlRight := ltac2:(mlRight ()).
Local Example ex_mlLeft {Σ : Signature} Γ a:
well_formed a →
Γ ⊢i a ---> (a or a)
using BasicReasoning.
Lemma MLGoal_applyMetaIn {Σ : Signature} Γ n r n' r' i:
Γ ⊢i (r ---> r') using i →
∀ l₁ l₂ g,
mkMLGoal Σ Γ (l₁ ++ (mkNH _ n' r')::l₂) g i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ n r)::l₂ ) g i.
Ltac2 do_mlApplyMetaRawIn (t : constr) (name : constr) :=
eapply cast_proof_ml_hyps;
f_equal;
run_in_reshaped_by_name name (fun () ⇒
eapply (@MLGoal_applyMetaIn _ _ _ _ $name _ _ $t)
)
.
Ltac do_mlApplyMetaRawIn t name :=
let f := ltac2:(t name |- do_mlApplyMetaRawIn (Option.get (Ltac1.to_constr t)) (Option.get (Ltac1.to_constr name))) in
f t name
.
Ltac2 do_mlApplyMetaRaw0 (t : constr) (cl : constr option) :=
match cl with
| None ⇒ do_mlApplyMetaRaw t
| Some n ⇒ do_mlApplyMetaRawIn t n
end
.
Ltac2 Notation "_mlApplyMetaRaw" t(constr) cl(opt(seq("in", constr))) :=
do_mlApplyMetaRaw0 t cl
.
Tactic Notation "mlApplyMetaRaw" constr(t) "in" constr(name) :=
let f := ltac2:(t name |- do_mlApplyMetaRawIn (Option.get (Ltac1.to_constr t)) (Option.get (Ltac1.to_constr name))) in
f t name
.
Local Example Private_ex_mlApplyMetaRawIn {Σ : Signature} Γ p q:
well_formed p →
well_formed q →
Γ ⊢i p ---> (p or q)
using BasicReasoning.
Ltac2 rec applyRec (f : constr) (xs : constr list) : constr option :=
match xs with
| [] ⇒ Some f
| y::ys ⇒
lazy_match! Constr.type f with
| (∀ _ : _, _) ⇒
Control.plus (fun () ⇒ applyRec constr:($f $y) ys) (fun _ ⇒ None)
| _ ⇒ None
end
end.
Ltac2 Eval (applyRec constr:(Nat.add) [constr:(1);constr:(2)]).
(*
All thic complicated code is here only for one reason:
I want to be able to first run the tactic with all the parameters
inferred or question marked, which results in another goal.
And then I want to handle the subgoals generated by the filling-in
underscores / question marks.
In particular, I want the proof mode goals to be generated first,
and the other, uninteresting goals, next.
*)
Ltac2 rec fillWithUnderscoresAndCall0
(tac : constr → unit) (t : constr) (args : constr list) :=
(*
Message.print (
Message.concat
(Message.of_string "fillWithUnderscoresAndCall: t = ")
(Message.of_constr t)
);
Message.print (
Message.concat
(Message.of_string "fillWithUnderscoresAndCall: args = ")
(List.fold_right (Message.concat) (Message.of_string "") (List.map Message.of_constr args))
);
*)
let cont := (fun () ⇒
lazy_match! Constr.type t with
| (?t' → ?_t's) ⇒ (* NOTE, (COQ BUG?) If I omit ?t's from here,
forall withh match this branch
NOTE2: This matching is fragile. Implication
hypotheses also seem to match the second branch
with forall _ : _ , _*)
lazy_match! goal with
| [|- ?g] ⇒
let h := Fresh.in_goal ident:(hasserted) in
assert($h : $t' → $g) > [(
let pftprime := Fresh.in_goal ident:(pftprime) in
intro $pftprime;
let new_t := open_constr:($t ltac2:(Notations.exact0 false (fun () ⇒ Control.hyp (pftprime)))) in
fillWithUnderscoresAndCall0 tac new_t args;
Std.clear [pftprime]
)|(
let h_constr := Control.hyp h in
apply $h_constr
)
]
end
| (∀ _ : _, _) ⇒ fillWithUnderscoresAndCall0 tac open_constr:($t _) args
| ?remainder ⇒ Control.throw (Invalid_argument (Some (Message.concat (Message.concat (Message.of_string "Remainder type: ") (Message.of_constr remainder)) (Message.concat (Message.of_string ", of term") (Message.of_constr t)))))
end
) in
match (applyRec t args) with
| None ⇒
(* Cannot apply t to args => continue *)
cont ()
| Some result ⇒
(* Can apply to to args, *)
lazy_match! Constr.type result with
| (∀ _ : _, _) ⇒
(* but result would still accept an argument => continue *)
cont ()
| _ ⇒
(* and nothing more can be applied to the result => we are done *)
tac result
end
end
.
Ltac2 rec fillWithUnderscoresAndCall
(tac : constr → unit) (twb : Std.constr_with_bindings) (args : constr list)
:=
let t := Fresh.in_goal ident:(t) in
Notations.specialize0 (fun () ⇒ twb) (Some (Std.IntroNaming (Std.IntroIdentifier t)));
let t_constr := Control.hyp t in
fillWithUnderscoresAndCall0 tac t_constr args;
clear $t
.
(*
We have this double-primed version because we want to be able
to feed it the proof before feeding it the ProofInfoLe.
*)
Lemma useGenericReasoning'' {Σ : Signature} (Γ : Theory) (ϕ : Pattern) i' i:
Γ ⊢i ϕ using i' →
(ProofInfoLe i' i) →
Γ ⊢i ϕ using i.
(* TODO: Create error messages for the following tactics *)
Ltac2 _callCompletedAndCast (twb : Std.constr_with_bindings) (tac : constr → unit) :=
let tac' := (fun (t' : constr) ⇒
let tcast := open_constr:(@useGenericReasoning'' _ _ _ _ _ $t') in
fillWithUnderscoresAndCall0 tac tcast []
) in
let t := Fresh.in_goal ident:(t) in
Notations.specialize0 (fun () ⇒ twb) (Some (Std.IntroNaming (Std.IntroIdentifier t)));
let t_constr := Control.hyp t in
fillWithUnderscoresAndCall0 tac' t_constr [];
clear $t
.
Ltac2 try_solve_pile_basic () :=
Control.enter (fun () ⇒
lazy_match! goal with
| [ |- (@ProofInfoLe _ _ _)] ⇒
try (solve
[ apply pile_any
| apply pile_refl
| apply pile_basic_generic
])
| [|- _] ⇒ ()
end
)
.
Ltac2 try_wfa () :=
Control.enter (fun () ⇒
let wfa := (fun p ⇒
if (Constr.has_evar p) then
()
else
ltac1:(try_wfauto2)
) in
lazy_match! goal with
| [|- well_formed ?p = true] ⇒ wfa p
| [|- is_true (well_formed ?p) ] ⇒ wfa p
| [|- Pattern.wf ?l = true] ⇒ wfa l
| [|- is_true (Pattern.wf ?l) ] ⇒ wfa l
| [|- _] ⇒ ()
end
)
.
Ltac2 mutable do_mlApplyMeta := fun (twb : Std.constr_with_bindings) ⇒
Control.enter (fun () ⇒
_ensureProofMode;
_callCompletedAndCast twb do_mlApplyMetaRaw ;
try_solve_pile_basic ();
try_wfa ()
)
.
Ltac2 mutable do_mlApplyMetaIn := fun (twb : Std.constr_with_bindings) (name : constr) ⇒
Control.enter (fun () ⇒
_ensureProofMode;
_callCompletedAndCast twb (fun t ⇒
do_mlApplyMetaRawIn t name
);
try_solve_pile_basic ();
try_wfa ()
)
.
Ltac2 do_mlApplyMeta0 (twb : Std.constr_with_bindings) (cl : constr option) :=
match cl with
| None ⇒ do_mlApplyMeta twb
| Some n ⇒ do_mlApplyMetaIn twb n
end
.
Ltac2 Notation "mlApplyMeta" t(seq(constr,with_bindings)) cl(opt(seq("in", constr))) :=
do_mlApplyMeta0 t cl
.
Ltac _mlApplyMeta t :=
let ff := ltac2:(t' |- do_mlApplyMeta ((Option.get (Ltac1.to_constr(t'))), Std.NoBindings)) in
ff t.
Ltac _mlApplyMetaIn t name :=
let ff := ltac2:(t' name' |- do_mlApplyMetaIn ((Option.get (Ltac1.to_constr(t')), Std.NoBindings)) (Option.get (Ltac1.to_constr(name')))) in
ff t name
.
Tactic Notation "mlApplyMeta" constr(t) :=
_mlApplyMeta t.
Tactic Notation "mlApplyMeta" constr(t) "in" constr(name) :=
_mlApplyMetaIn t name
.
Lemma MLGoal_destructAnd {Σ : Signature} Γ g l₁ l₂ nx x ny y nxy i:
mkMLGoal Σ Γ (l₁ ++ (mkNH _ nx x)::(mkNH _ ny y)::l₂ ) g i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ nxy (x and y))::l₂) g i.
Ltac2 mlDestructAnd_as (name : constr) (name1 : constr) (name2 : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
_failIfUsed $name1;
_failIfUsed $name2;
run_in_reshaped_by_name name (fun () ⇒
Control.plus(fun () ⇒
apply MLGoal_destructAnd with (nxy := $name) (nx := $name1) (ny := $name2)
)
(fun _ ⇒
_mlReshapeHypsBack;
throw_pm_exn_with_goal "mlDestructAnd_as: Given matching logic hypothesis is not a conjunction! ")
)
)
.
Ltac2 Notation "mlDestructAnd" name(constr) "as" name1(constr) name2(constr) :=
mlDestructAnd_as name name1 name2
.
Tactic Notation "mlDestructAnd" constr(name) "as" constr(name1) constr(name2) :=
let f := ltac2:(name name1 name2 |- mlDestructAnd_as (Option.get (Ltac1.to_constr name)) (Option.get (Ltac1.to_constr name1)) (Option.get (Ltac1.to_constr name2))) in
f name name1 name2
.
Ltac2 do_mlDestructAnd (name : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
let hyps := do_getHypNames () in
let name0 := eval cbv in (fresh $hyps) in
let name1 := eval cbv in (fresh ($name0 :: $hyps)) in
mlDestructAnd $name as $name0 $name1
)
.
Ltac2 Notation "mlDestructAnd" name(constr) :=
do_mlDestructAnd name
.
Tactic Notation "mlDestructAnd" constr(name) :=
let f := ltac2:(name |- do_mlDestructAnd (Option.get (Ltac1.to_constr name))) in
f name
.
Local Example ex_mlDestructAnd {Σ : Signature} Γ a b p q:
well_formed a →
well_formed b →
well_formed p →
well_formed q →
Γ ⊢i p and q ---> a and b ---> q ---> a
using BasicReasoning.
Lemma and_of_equiv_is_equiv {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i (p <---> p') using i →
Γ ⊢i (q <---> q') using i →
Γ ⊢i ((p and q) <---> (p' and q')) using i.
Lemma or_of_equiv_is_equiv {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i (p <---> p') using i →
Γ ⊢i (q <---> q') using i →
Γ ⊢i ((p or q) <---> (p' or q')) using i.
Lemma impl_iff_notp_or_q {Σ : Signature} Γ p q:
well_formed p →
well_formed q →
Γ ⊢i ((p ---> q) <---> (! p or q))
using BasicReasoning.
Lemma p_and_notp_is_bot {Σ : Signature} Γ p:
well_formed p →
Γ ⊢i (⊥ <---> p and ! p)
using BasicReasoning.
Ltac2 do_mlExFalso ():=
_ensureProofMode;
mlApplyMeta bot_elim
.
Ltac2 Notation "mlExFalso"
:= do_mlExFalso ()
.
Ltac mlExFalso :=
ltac2:(do_mlExFalso ())
.
Ltac2 do_mlDestructBot (name' : constr) :=
Control.enter(fun () ⇒
run_in_reshaped_by_name name' (fun () ⇒
mlExFalso;
do_mlExact name'
)
)
.
Ltac2 Notation "mlDestructBot" name(constr) :=
do_mlDestructBot name
.
Tactic Notation "mlDestructBot" constr(name') :=
let f := ltac2:(name |- do_mlDestructBot (Option.get (Ltac1.to_constr name))) in
f name'
.
Lemma weird_lemma {Σ : Signature} Γ A B L R:
well_formed A →
well_formed B →
well_formed L →
well_formed R →
Γ ⊢i (((L and A) ---> (B or R)) ---> (L ---> ((A ---> B) or R)))
using BasicReasoning.
Lemma weird_lemma_meta {Σ : Signature} Γ A B L R i:
well_formed A →
well_formed B →
well_formed L →
well_formed R →
Γ ⊢i ((L and A) ---> (B or R)) using i →
Γ ⊢i (L ---> ((A ---> B) or R)) using i.
Lemma imp_trans_mixed_meta {Σ : Signature} Γ A B C D i :
well_formed A → well_formed B → well_formed C → well_formed D →
Γ ⊢i (C ---> A) using i →
Γ ⊢i (B ---> D) using i →
Γ ⊢i ((A ---> B) ---> C ---> D) using i.
Lemma and_weaken {Σ : Signature} A B C Γ i:
well_formed A → well_formed B → well_formed C →
Γ ⊢i (B ---> C) using i →
Γ ⊢i ((A and B) ---> (A and C)) using i.
Lemma impl_and {Σ : Signature} Γ A B C D i:
well_formed A → well_formed B → well_formed C → well_formed D →
Γ ⊢i (A ---> B) using i →
Γ ⊢i (C ---> D) using i →
Γ ⊢i (A and C) ---> (B and D) using i.
Lemma and_drop {Σ : Signature} A B C Γ i:
well_formed A → well_formed B → well_formed C →
Γ ⊢i ((A and B) ---> C) using i →
Γ ⊢i ((A and B) ---> (A and C)) using i.
Lemma prf_equiv_of_impl_of_equiv {Σ : Signature} Γ a b a' b' i:
well_formed a = true →
well_formed b = true →
well_formed a' = true →
well_formed b' = true →
Γ ⊢i (a <---> a') using i →
Γ ⊢i (b <---> b') using i →
Γ ⊢i (a ---> b) <---> (a' ---> b') using i.
Lemma lhs_to_and {Σ : Signature} Γ a b c i:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i (a and b) ---> c using i →
Γ ⊢i a ---> b ---> c using i.
Lemma lhs_from_and {Σ : Signature} Γ a b c i:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i a ---> b ---> c using i →
Γ ⊢i (a and b) ---> c using i.
Lemma prf_conj_split {Σ : Signature} Γ a b l:
well_formed a →
well_formed b →
Pattern.wf l →
Γ ⊢i (foldr patt_imp a l) ---> (foldr patt_imp b l) ---> (foldr patt_imp (a and b) l)
using BasicReasoning.
Lemma prf_conj_split_meta {Σ : Signature} Γ a b l (i : ProofInfo):
well_formed a →
well_formed b →
Pattern.wf l →
Γ ⊢i (foldr patt_imp a l) using i →
Γ ⊢i (foldr patt_imp b l) ---> (foldr patt_imp (a and b) l) using i.
Lemma prf_conj_split_meta_meta {Σ : Signature} Γ a b l (i : ProofInfo):
well_formed a →
well_formed b →
Pattern.wf l →
Γ ⊢i (foldr patt_imp a l) using i →
Γ ⊢i (foldr patt_imp b l) using i →
Γ ⊢i (foldr patt_imp (a and b) l) using i.
Lemma MLGoal_splitAnd {Σ : Signature} Γ a b l i:
mkMLGoal Σ Γ l a i →
mkMLGoal Σ Γ l b i →
mkMLGoal Σ Γ l (a and b) i.
Ltac2 do_mlSplitAnd () :=
Control.enter(fun () ⇒
_ensureProofMode;
Control.plus(fun () ⇒
apply MLGoal_splitAnd
)
(fun _ ⇒ throw_pm_exn_with_goal "do_mlSplitAnd: matching logic goal is not a conjunction! ")
)
.
Ltac2 Notation "mlSplitAnd" :=
do_mlSplitAnd ()
.
Ltac mlSplitAnd :=
ltac2:(do_mlSplitAnd ())
.
Local Lemma ex_mlSplitAnd {Σ : Signature} Γ a b c:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i a ---> b ---> c ---> (a and b)
using BasicReasoning.
Lemma prf_local_goals_equiv_impl_full_equiv {Σ : Signature} Γ g₁ g₂ l:
well_formed g₁ →
well_formed g₂ →
Pattern.wf l →
Γ ⊢i (foldr patt_imp (g₁ <---> g₂) l) --->
((foldr patt_imp g₁ l) <---> (foldr patt_imp g₂ l))
using BasicReasoning.
Lemma prf_local_goals_equiv_impl_full_equiv_meta {Σ : Signature} Γ g₁ g₂ l i:
well_formed g₁ →
well_formed g₂ →
Pattern.wf l →
Γ ⊢i (foldr patt_imp (g₁ <---> g₂) l) using i →
Γ ⊢i ((foldr patt_imp g₁ l) <---> (foldr patt_imp g₂ l)) using i.
Lemma prf_local_goals_equiv_impl_full_equiv_meta_proj1 {Σ : Signature} Γ g₁ g₂ l i:
well_formed g₁ →
well_formed g₂ →
Pattern.wf l →
Γ ⊢i (foldr patt_imp (g₁ <---> g₂) l) using i →
Γ ⊢i (foldr patt_imp g₁ l) using i →
Γ ⊢i (foldr patt_imp g₂ l) using i.
Lemma prf_local_goals_equiv_impl_full_equiv_meta_proj2 {Σ : Signature} Γ g₁ g₂ l i:
well_formed g₁ →
well_formed g₂ →
Pattern.wf l →
Γ ⊢i (foldr patt_imp (g₁ <---> g₂) l) using i →
Γ ⊢i (foldr patt_imp g₂ l) using i →
Γ ⊢i (foldr patt_imp g₁ l) using i.
Lemma top_holds {Σ : Signature} Γ:
Γ ⊢i Top using BasicReasoning.
Lemma phi_iff_phi_top {Σ : Signature} Γ ϕ :
well_formed ϕ →
Γ ⊢i ϕ <---> (ϕ <---> Top)
using BasicReasoning.
Lemma not_phi_iff_phi_bott {Σ : Signature} Γ ϕ :
well_formed ϕ →
Γ ⊢i (! ϕ ) <---> (ϕ <---> ⊥)
using BasicReasoning.
Lemma not_not_iff {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i A <---> ! ! A
using BasicReasoning.
Lemma patt_and_comm {Σ : Signature} Γ p q:
well_formed p →
well_formed q →
Γ ⊢i (p and q) <---> (q and p)
using BasicReasoning.
(* We need to come up with tactics that make this easier. *)
Local Example ex_mt {Σ : Signature} Γ ϕ₁ ϕ₂:
well_formed ϕ₁ →
well_formed ϕ₂ →
Γ ⊢i (! ϕ₁ ---> ! ϕ₂) ---> (ϕ₂ ---> ϕ₁)
using BasicReasoning.
Lemma lhs_and_to_imp {Σ : Signature} Γ (g x : Pattern) (xs : list Pattern):
well_formed g →
well_formed x →
Pattern.wf xs →
Γ ⊢i (foldr patt_and x xs ---> g) ---> (foldr patt_imp g (x :: xs))
using BasicReasoning.
Lemma lhs_and_to_imp_meta {Σ : Signature} Γ (g x : Pattern) (xs : list Pattern) i:
well_formed g →
well_formed x →
Pattern.wf xs →
Γ ⊢i (foldr patt_and x xs ---> g) using i →
Γ ⊢i (foldr patt_imp g (x :: xs)) using i.
Lemma lhs_imp_to_and {Σ : Signature} Γ (g x : Pattern) (xs : list Pattern):
well_formed g →
well_formed x →
Pattern.wf xs →
Γ ⊢i (foldr patt_imp g (x :: xs)) ---> (foldr patt_and x xs ---> g)
using BasicReasoning.
Lemma lhs_imp_to_and_meta {Σ : Signature} Γ (g x : Pattern) (xs : list Pattern) i:
well_formed g →
well_formed x →
Pattern.wf xs →
Γ ⊢i (foldr patt_imp g (x :: xs)) using i →
Γ ⊢i (foldr patt_and x xs ---> g) using i.
Lemma foldr_and_impl_last {Σ : Signature} Γ (x : Pattern) (xs : list Pattern):
well_formed x →
Pattern.wf xs →
Γ ⊢i (foldr patt_and x xs ---> x) using BasicReasoning.
Lemma foldr_and_weaken_last {Σ : Signature} Γ (x y : Pattern) (xs : list Pattern):
well_formed x →
well_formed y →
Pattern.wf xs →
Γ ⊢i (x ---> y) ---> (foldr patt_and x xs ---> foldr patt_and y xs) using BasicReasoning.
Lemma foldr_and_weaken_last_meta {Σ : Signature} Γ (x y : Pattern) (xs : list Pattern) i:
well_formed x →
well_formed y →
Pattern.wf xs →
Γ ⊢i (x ---> y) using i →
Γ ⊢i (foldr patt_and x xs ---> foldr patt_and y xs) using i.
Lemma foldr_and_last_rotate {Σ : Signature} Γ (x1 x2 : Pattern) (xs : list Pattern):
well_formed x1 →
well_formed x2 →
Pattern.wf xs →
Γ ⊢i ((foldr patt_and x2 (xs ++ [x1])) <---> (x2 and (foldr patt_and x1 xs))) using BasicReasoning.
Lemma foldr_and_last_rotate_1 {Σ : Signature} Γ (x1 x2 : Pattern) (xs : list Pattern):
well_formed x1 →
well_formed x2 →
Pattern.wf xs →
Γ ⊢i ((foldr patt_and x2 (xs ++ [x1])) ---> (x2 and (foldr patt_and x1 xs))) using BasicReasoning.
Lemma foldr_and_last_rotate_2 {Σ : Signature} Γ (x1 x2 : Pattern) (xs : list Pattern):
well_formed x1 →
well_formed x2 →
Pattern.wf xs →
Γ ⊢i ((x2 and (foldr patt_and x1 xs)) ---> ((foldr patt_and x2 (xs ++ [x1])))) using BasicReasoning.
#[local]
Ltac2 rec tryExact (l : constr) (idx : constr) :=
lazy_match! l with
| nil ⇒ throw_pm_exn_with_goal "tryExact: there was no matching logic hypothesis which is exactly matched by the goal: "
| (_ :: ?m) ⇒ Control.plus (fun () ⇒ do_mlExactn idx) (fun _ ⇒ tryExact m constr:($idx + 1))
end.
#[global]
Ltac2 do_mlAssumption () :=
Control.enter(fun () ⇒
_ensureProofMode;
lazy_match! goal with
| [ |- @of_MLGoal _ (@mkMLGoal _ _ ?l _ _) ]
⇒
tryExact l constr:(0)
end
)
.
Ltac2 Notation "mlAssumption" :=
do_mlAssumption ()
.
Tactic Notation "mlAssumption" :=
ltac2:(do_mlAssumption ())
.
Lemma impl_eq_or {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( (a ---> b) <---> ((! a) or b) )
using BasicReasoning.
Lemma nimpl_eq_and {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( ! (a ---> b) <---> (a and !b) )
using BasicReasoning.
Lemma deMorgan_nand_1 {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( !(a and b) ---> (!a or !b) )
using BasicReasoning.
Lemma deMorgan_nand_2 {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( (!a or !b) ---> !(a and b) )
using BasicReasoning.
Lemma deMorgan_nand {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( !(a and b) <---> (!a or !b) )
using BasicReasoning.
Lemma deMorgan_nor_1 {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( !(a or b) ---> (!a and !b))
using BasicReasoning.
Lemma deMorgan_nor_2 {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( (!a and !b) ---> !(a or b))
using BasicReasoning.
Lemma deMorgan_nor {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( !(a or b) <---> (!a and !b))
using BasicReasoning.
Lemma not_not_eq {Σ : Signature} (Γ : Theory) (a : Pattern) :
well_formed a →
Γ ⊢i (!(!a) <---> a)
using BasicReasoning.
Lemma and_singleton {Σ : Signature} : ∀ Γ p,
well_formed p → Γ ⊢i (p and p) <---> p using BasicReasoning.
Lemma bott_and {Σ : Signature} Γ ϕ :
well_formed ϕ →
Γ ⊢ ⊥ and ϕ <---> ⊥.
Lemma top_and {Σ : Signature} Γ ϕ :
well_formed ϕ →
Γ ⊢ Top and ϕ <---> ϕ.
Lemma MLGoal_ExactMeta {Σ:Signature} : ∀ Γ l g i,
Γ ⊢i g using i →
mkMLGoal Σ Γ l g i.
Tactic Notation "mlExactMeta" uconstr(t) :=
_ensureProofMode;
apply (@MLGoal_ExactMeta _ _ _ _ _ t).
Goal ∀ (Σ : Signature) Γ, Γ ⊢i Top using BasicReasoning.
Local Example exfalso_test {Σ : Signature} p Γ i :
well_formed p →
Γ ⊢i p and ! p ---> Top using i.
Local Example destruct_bot_test {Σ : Signature} p Γ i :
well_formed p →
Γ ⊢i ⊥ ---> Top using i.
Lemma extract_common_from_equivalence
{Σ : Signature} (Γ : Theory) (a b c : Pattern):
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i (((a and b) <---> (a and c)) <---> (a ---> (b <---> c)))
using BasicReasoning
.
Lemma extract_common_from_equivalence_1
{Σ : Signature} (Γ : Theory) (a b c : Pattern):
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i ((a ---> (b <---> c)) ---> ((a and b) <---> (a and c)))
using BasicReasoning
.
Lemma extract_common_from_equivalence_2
{Σ : Signature} (Γ : Theory) (a b c : Pattern):
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i (((a and b) <---> (a and c)) ---> (a ---> (b <---> c)))
using BasicReasoning
.
Ltac2 do_mlClassic_as (p : constr) (n1 : constr) (n2 : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
let hyps := do_getHypNames () in
let tmpName := eval cbv in (fresh $hyps) in
let wfName := Fresh.in_goal ident:(Hwf) in
lazy_match! goal with
| [|- @of_MLGoal _ (@mkMLGoal _ ?ctx ?_l ?_g ?i)]
⇒ assert ($wfName : well_formed $p = true)>
[()|(
let wf_hyp := Control.hyp wfName in
mlAdd (useBasicReasoning $i (A_or_notA $ctx $p $wf_hyp)) as $tmpName;
mlDestructOr $tmpName as $n1 $n2
)]
end
)
.
Ltac2 Notation "mlClassic" p(constr) "as" n1(constr) n2(constr) :=
do_mlClassic_as p n1 n2
.
Tactic Notation "mlClassic" constr(p) "as" constr(n1) constr(n2) :=
let f := ltac2:(p n1 n2 |- do_mlClassic_as (Option.get (Ltac1.to_constr p)) (Option.get (Ltac1.to_constr n1)) (Option.get (Ltac1.to_constr n2))) in
f p n1 n2
.
#[local]
Example exMlClassic {Σ : Signature} (Γ : Theory) (a : Pattern):
well_formed a →
Γ ⊢ (a or !a).
Lemma prf_clear_hyps_meta {Σ : Signature} Γ l1 l2 l3 g i:
Pattern.wf l1 →
Pattern.wf l2 →
Pattern.wf l3 →
well_formed g →
Γ ⊢i (foldr patt_imp g (l1 ++ l3)) using i →
Γ ⊢i (foldr patt_imp g (l1 ++ l2 ++ l3)) using i.
Lemma MLGoal_ApplyIn {Σ : Signature} Γ l1 l2 l3 name1 name2 h h' g i:
mkMLGoal Σ Γ (l1 ++ (mkNH _ name1 h') :: l2 ++ (mkNH _ name2 (h ---> h')) :: l3) g i →
mkMLGoal Σ Γ (l1 ++ (mkNH _ name1 h) :: l2 ++ (mkNH _ name2 (h ---> h')) :: l3) g i.
Lemma MLGoal_Swap {Σ : Signature} Γ l1 l2 l3 name1 name2 h1 h2 g i:
mkMLGoal Σ Γ (l1 ++ (mkNH _ name1 h1) :: l2 ++ (mkNH _ name2 h2) :: l3) g i →
mkMLGoal Σ Γ (l1 ++ (mkNH _ name2 h2) :: l2 ++ (mkNH _ name1 h1) :: l3) g i.
Ltac2 do_mlSwap (n1 : constr) (n2 : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
_mlReshapeHypsBy2Names n1 n2;
apply MLGoal_Swap;
_mlReshapeHypsBackTwice
)
.
Ltac2 Notation "mlSwap" n1(constr) "with" n2(constr) :=
do_mlSwap n1 n2.
Tactic Notation "mlSwap" constr(n1) "with" constr(n2) :=
let f := ltac2:(n1 n2 |- do_mlSwap (Option.get (Ltac1.to_constr n1)) (Option.get (Ltac1.to_constr n2))) in
f n1 n2.
Ltac2 do_mlApplyIn (name1' : constr) (name2' : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
_mlReshapeHypsBy2Names name1' name2';
(
(* Check the order of the hypotheses *)
match! goal with
| [ |- @of_MLGoal _ (@mkMLGoal _ _ (_ ++ ((@mkNH _ _ ?_h :: _) ++ (@mkNH _ _ (?_h ---> _) :: _))) _ _) ] ⇒
apply MLGoal_ApplyIn;
_mlReshapeHypsBackTwice
| [ |- _ ] ⇒ _mlReshapeHypsBackTwice;
mlSwap $name1' with $name2';
_mlReshapeHypsBy2Names name2' name1' ;
apply MLGoal_ApplyIn;
_mlReshapeHypsBackTwice;
mlSwap $name1' with $name2'
end
)
)
.
Ltac2 Notation "mlApply" n1(constr) "in" n2(constr) :=
do_mlApplyIn n1 n2.
Tactic Notation "mlApply" constr(name1') "in" constr(name2') :=
let f := ltac2:(name1' name2' |- do_mlApplyIn (Option.get (Ltac1.to_constr name1')) (Option.get (Ltac1.to_constr name2'))) in
f name1' name2'.
Example ex_mlApplyIn {Σ : Signature} Γ a b c d e f i:
well_formed a → well_formed b →
well_formed c → well_formed d →
well_formed e → well_formed f →
Γ ⊢i (c---> a ---> c ---> (a ---> b) ---> a ---> b) using i.
Lemma MLGoal_conjugate_hyps {Σ : Signature}
(Γ : Theory)
(l1 l2 l3 : hypotheses)
(name1 name2 conj_name : string)
(goal p1 p2 : Pattern)
(info : ProofInfo):
(* well_formed p1 -> well_formed p2 ->
Pattern.wf (map nh_patt (l1 ++ l2 ++ l3)) -> *)
mkMLGoal Σ Γ ((mkNH _ conj_name (p1 and p2)) :: (l1 ++ (mkNH _ name1 p1) :: l2 ++ (mkNH _ name2 p2) :: l3)) goal info →
mkMLGoal Σ Γ (l1 ++ (mkNH _ name1 p1) :: l2 ++ (mkNH _ name2 p2) :: l3) goal info.
Lemma patt_and_comm_basic {Σ : Signature}
(Γ : Theory)
(φ1 φ2 : Pattern) :
well_formed φ1 → well_formed φ2 →
Γ ⊢i φ1 and φ2 ---> φ2 and φ1 using BasicReasoning.
Ltac2 do_mlConj (n1 : constr) (n2 : constr) (conj_name' : constr) :=
Control.enter(fun () ⇒
_ensureProofMode;
do_failIfUsed conj_name';
_mlReshapeHypsBy2Names n1 n2;
apply MLGoal_conjugate_hyps with (conj_name := $conj_name');
rewrite app_comm_cons;
_mlReshapeHypsBackTwice;
lazy_match! goal with
| [ |- @of_MLGoal _ (@mkMLGoal _ _ ?l _ _) ] ⇒
lazy_match! eval cbv in (index_of $n1 (names_of $l)) with
| (Some ?i1) ⇒
lazy_match! eval cbv in (index_of $n2 (names_of $l)) with
| (Some ?i2) ⇒
lazy_match! (eval cbv in (Nat.compare $i1 $i2)) with
| (Lt) ⇒ ()
| (Gt) ⇒ mlApplyMeta patt_and_comm_basic in $conj_name'
| (Eq) ⇒ throw_pm_exn_with_goal "do_mlConj: Equal names were used"
end
| (None) ⇒ throw_pm_exn (Message.concat (Message.of_string "do_mlConj: No such name: ") (Message.of_constr n2))
end
| (None) ⇒ throw_pm_exn (Message.concat (Message.of_string "do_mlConj: No such name: ") (Message.of_constr n1))
end
end
).
Ltac2 Notation "mlConj" n1(constr) n2(constr) "as" n3(constr) :=
do_mlConj n1 n2 n3.
Tactic Notation "mlConj" constr(n1) constr(n2) "as" constr(n3) :=
let f := ltac2:(n1 n2 n3 |- do_mlConj (Option.get (Ltac1.to_constr n1)) (Option.get (Ltac1.to_constr n2)) (Option.get (Ltac1.to_constr n3))) in
f n1 n2 n3.
Ltac2 rec do_mlConj_many l (name : constr) : unit :=
match l with
| [] ⇒ throw_pm_exn (Message.of_string "do_mlConj_many: empty list")
| a :: t1 ⇒
match t1 with
| [] ⇒ throw_pm_exn (Message.of_string "do_mlConj_many: singleton list")
| b :: t2 ⇒
match t2 with
| [] ⇒ mlConj $a $b as $name
| _ :: _ ⇒
do_mlConj_many t1 name;
let hyps := do_getHypNames () in
let newname := eval cbv in (fresh $hyps) in
(* rename name into newname
TODO: optimise this with mlRename, which is independent of ML proofs: *)
mlRename $name into $newname;
mlConj $a $newname as $name;
mlClear $newname
end
end
end.
Ltac2 Notation "mlConj" l(list1(constr, ",")) "as" n3(constr) :=
do_mlConj_many l n3.
(**********************************************************************************)
Example ex_ml_conj_intro {Σ : Signature} Γ a b c d e f i:
well_formed a → well_formed b →
well_formed c → well_formed d →
well_formed e → well_formed f →
Γ ⊢i (a ---> b ---> c ---> d ---> e ---> f ---> (b and e)) using i.
Example ex_ml_conj_many_intro {Σ : Signature} Γ a b c d e f i:
well_formed a → well_formed b →
well_formed c → well_formed d →
well_formed e → well_formed f →
Γ ⊢i a ---> b ---> c ---> d ---> e ---> f ---> (a and (b and (c and e))) using i.
(* This is an example and belongs to the end of this file.
Its only purpose is only to show as many tactics as possible.\
*)
Example ex_and_of_equiv_is_equiv_2 {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i (p <---> p') using i →
Γ ⊢i (q <---> q') using i →
Γ ⊢i ((p and q) <---> (p' and q')) using i.
#[local]
Example ex_or_of_equiv_is_equiv_2 {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i (p <---> p') using i →
Γ ⊢i (q <---> q') using i →
Γ ⊢i ((p or q) <---> (p' or q')) using i.
Class MLReflexive {Σ : Signature} (op : Pattern → Pattern → Pattern) := {
reflexive_op_well_formed : ∀ φ ψ,
well_formed (op φ ψ) → well_formed φ ∧ well_formed ψ;
mlReflexivity :
∀ Γ φ i, well_formed φ → Γ ⊢i op φ φ using i;
}.
#[global]
Instance patt_imp_is_reflexive {Σ : Signature} : @MLReflexive Σ patt_imp.
#[export]
Hint Resolve patt_imp_is_reflexive : core.
#[global]
Instance patt_iff_is_reflexive {Σ : Signature} : @MLReflexive Σ patt_iff.
#[export]
Hint Resolve patt_iff_is_reflexive : core.
Lemma MLGoal_reflexivity {Σ : Signature} Γ l φ i op {_ : MLReflexive op} :
mkMLGoal _ Γ l (op φ φ) i.
Ltac2 do_mlReflexivity () :=
Control.enter(fun () ⇒
_ensureProofMode;
lazy_match! goal with
| [ |- @of_MLGoal _ (@mkMLGoal _ _ _ (?op ?_g ?_g) _) ] ⇒
match! goal with (* error handling *)
| [ |- _] ⇒ now (apply MLGoal_reflexivity; eauto)
| [ |- _] ⇒
throw_pm_exn
(Message.concat (Message.of_string "do_mlReflexivity: ")
(Message.concat (Message.of_constr op) (Message.of_string " is not reflexive!"))
)
end
| [ |- _] ⇒ Message.print (Message.of_string "Goal is not shaped as φ = φ!"); fail
end
).
Ltac2 Notation "mlReflexivity" :=
do_mlReflexivity ().
Tactic Notation "mlReflexivity" :=
ltac2:(do_mlReflexivity ()).
#[local]
Example reflexive_imp_test1 {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i p ---> p using i.
#[local]
Example notreflexive_and_test1 {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i p and p using i.
#[local]
Example reflexive_imp_test2 {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i q ---> q' ---> p' ---> p ---> p using i.
#[local]
Example reflexive_iff_test {Σ : Signature} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i q ---> q' ---> p' ---> p <---> p using i.
Lemma pf_iff_equiv_trans_obj {Σ : Signature} : ∀ Γ A B C i,
well_formed A → well_formed B → well_formed C →
Γ ⊢i (A <---> B) ---> (B <---> C) ---> (A <---> C) using i.
Lemma pf_iff_equiv_sym_obj {Σ : Signature} Γ A B i :
well_formed A → well_formed B → Γ ⊢i (A <---> B) ---> (B <---> A) using i.
(* TODO: make for other transitive relations too, then maybe move *)
Tactic Notation "mlTrans_iff" constr(b) :=
match goal with
| [ |- context[(mkMLGoal _ ?g ?h (patt_iff ?a ?c) ?i)] ] ⇒
let Htrans := fresh in
opose proof× (pf_iff_equiv_trans_obj g a b c i _ _ _) as Htrans;
last (
let Htrans2 := eval cbv in (fresh (map nh_name h)) in (
mlAssert (Htrans2 : (a <---> b));
last (
mlApplyMeta Htrans in Htrans2;
mlApply Htrans2;
mlClear Htrans2
)
);
last 2 [clear Htrans]
)
end.
Tactic Notation "emlTrans_iff" :=
let ep := fresh in
evar (ep : Pattern);
mlTrans_iff ep;
subst ep.
Lemma extract_common_from_equivalence_r {Σ : Signature} Γ a b c i :
well_formed a → well_formed b → well_formed c →
Γ ⊢i (b and a <---> c and a) <---> (a ---> b <---> c) using i.
Theorem provable_iff_top:
∀ {Σ : Signature} (Γ : Theory) (φ : Pattern) (i : ProofInfo),
well_formed φ →
Γ ⊢i φ using i →
Γ ⊢i φ <---> patt_top using i .
Theorem patt_and_id_r:
∀ {Σ : Signature} (Γ : Theory) (φ : Pattern),
well_formed φ →
Γ ⊢i φ and patt_top <---> φ using BasicReasoning .
This page has been generated by coqdoc