File Misc
From MatchingLogic Require Export FreshnessManager.
From MatchingLogic.ProofMode Require Export Reshaper FixPoint.
(*
Require Import wftactics2. *)
Import MatchingLogic.Logic.Notations.
Open Scope list_scope. (* needed for mlAssert, ++ *)
(* TODO: create error messages for these tactics *)
Ltac2 _callCompletedTransformedAndCast0
(t : constr) (transform : constr) (tac : constr → unit) :=
let tac' := (fun (t' : constr) ⇒
let tac'' := (fun (t'' : constr) ⇒
let tcast := open_constr:(@useGenericReasoning'' _ _ _ _ _ $t'') in
fillWithUnderscoresAndCall0 tac tcast []
) in
fillWithUnderscoresAndCall0 (fun t''' ⇒ tac'' t''') transform [t']
) in
fillWithUnderscoresAndCall0 tac' t []
.
Ltac2 _callCompletedTransformedAndCast
(twb : Std.constr_with_bindings) (transform : constr) (tac : constr → unit) :=
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
_callCompletedTransformedAndCast0 t_constr transform tac;
clear $t
.
Ltac2 do_mlApplyMetaGeneralized (twb : Std.constr_with_bindings) :=
Control.enter(fun () ⇒
_callCompletedTransformedAndCast twb constr:(@reshape_lhs_imp_to_and_forward) do_mlApplyMetaRaw ;
try_solve_pile_basic ();
try_wfa ();
ltac1:(rewrite [foldr patt_and _ _]/=)
)
.
Ltac2 Notation "mlApplyMetaGeneralized" t(seq(open_constr,with_bindings)) :=
do_mlApplyMetaGeneralized t
.
Tactic Notation "mlApplyMetaGeneralized" uconstr(t) :=
let f := ltac2:(t |- do_mlApplyMetaGeneralized ((Option.get (Ltac1.to_constr t)), Std.NoBindings)) in
f t
.
Ltac2 Set do_mlApplyMeta as old_do_mlApplyMeta := fun (twb : Std.constr_with_bindings) ⇒
orelse (fun () ⇒ old_do_mlApplyMeta twb) (fun _ ⇒ do_mlApplyMetaGeneralized twb)
.
#[local]
Example ex_mlApplyMetaGeneralized {Σ : Signature} Γ a b c d e f:
well_formed a →
well_formed b →
well_formed c →
well_formed d →
well_formed e →
well_formed f →
Γ ⊢ a ---> b ---> c ---> d ---> e ---> f →
Γ ⊢ (a and (b and (c and (d and e)))) ---> f.
#[local]
Example ex_mlApplyMetaGeneralized2 {Σ : Signature} Γ a b c d e f:
well_formed a →
well_formed b →
well_formed c →
well_formed d →
well_formed e →
well_formed f →
(∀ c', well_formed c' = true → Γ ⊢ a ---> b ---> c' ---> d ---> e ---> f) →
Γ ⊢ (a and (b and (c and (d and e)))) ---> f.
Lemma foldr_andb_init_true i l:
foldr andb i l = true → i = true.
Lemma foldr_andb_true_iff i l:
foldr andb i l = i && foldr andb true l.
Lemma MLGoal_weakenConclusionGen' {Σ : Signature} Γ l₁ l₂ name g' i
(x : Pattern) (xs : list Pattern)
:
∀ (r : ImpReshapeS g' (x::xs)),
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name ((untagPattern (irs_flattened _ _ r)))) :: l₂) ((foldr (patt_and) x xs)) i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name ((untagPattern (irs_flattened _ _ r)))) :: l₂) g' i.
Lemma MLGoal_weakenConclusionGen {Σ : Signature} Γ l₁ l₂ name g' i
(x : Pattern) (xs : list Pattern)
:
∀ (r : ImpReshapeS g' (x::xs)),
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name ((untagPattern (irs_flattened _ _ r)))) :: l₂)
(
match (rev xs) with
| [] ⇒ x
| yk::ys ⇒ (foldr (patt_and) yk (x::(rev ys)))
end
)
i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name ((untagPattern (irs_flattened _ _ r)))) :: l₂) g' i.
(* TODO: Reformulate this in Ltac2 *)
Tactic Notation "_mlApplyBasic" constr(name') :=
_ensureProofMode;
_mlReshapeHypsByName name';
tryif apply MLGoal_weakenConclusion;
_mlReshapeHypsBack
then idtac
else fail "_mlApplyBasic: Hypothesis does not match the goal".
(* TODO: Reformulate this in Ltac2 *)
Tactic Notation "_mlApplyGen" constr(name') :=
_ensureProofMode;
_mlReshapeHypsByName name';
tryif apply MLGoal_weakenConclusionGen;
_mlReshapeHypsBack
then idtac
else fail "_mlApplyGen: Hypothesis does not match the goal".
#[local]
Example ex_mlApplyGeneralized {Σ : Signature} Γ a b c d e f g:
well_formed a →
well_formed b →
well_formed c →
well_formed d →
well_formed e →
well_formed f →
well_formed g →
Γ ⊢ ((a and (b and (c and (d and e)))) --->
(a ---> b ---> c ---> d ---> e ---> f) --->
(f ---> g) --->
g).
Tactic Notation "mlApply" constr(name') :=
(_mlApplyBasic name') || (_mlApplyGen name')
.
Section FOL_helpers.
Context {Σ : Signature}.
Lemma Prop_bott_left (Γ : Theory) (ϕ : Pattern) :
well_formed ϕ →
Γ ⊢i ⊥ ⋅ ϕ ---> ⊥ using BasicReasoning.
Lemma Prop_bott_right (Γ : Theory) (ϕ : Pattern) :
well_formed ϕ →
Γ ⊢i ϕ ⋅ ⊥ ---> ⊥ using BasicReasoning.
Arguments Prop_bott_left _ (_%_ml) _ : clear implicits.
Arguments Prop_bott_right _ (_%_ml) _ : clear implicits.
Lemma Prop_bot_ctx (Γ : Theory) (C : Application_context) :
Γ ⊢i ((subst_ctx C patt_bott) ---> patt_bott)
using (ExGen := ∅, SVSubst := ∅, KT := false, AKT := false).
Lemma Framing (Γ : Theory) (C : Application_context) (A B : Pattern) (i : ProofInfo)
{pile : ProofInfoLe
((ExGen := ∅, SVSubst := ∅, KT := false, AKT := false))
i
}
:
Γ ⊢i (A ---> B) using i →
Γ ⊢i ((subst_ctx C A) ---> (subst_ctx C B)) using i.
Lemma A_implies_not_not_A_ctx (Γ : Theory) (A : Pattern) (C : Application_context)
(i : ProofInfo) {pile : ProofInfoLe ((ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)) i}
:
well_formed A →
Γ ⊢i A using i →
Γ ⊢i (! (subst_ctx C ( !A ))) using i.
Lemma ctx_bot_prop (Γ : Theory) (C : Application_context) (A : Pattern)
(i : ProofInfo)
{pile : ProofInfoLe ((ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)) i}
:
well_formed A →
Γ ⊢i (A ---> ⊥) using i →
Γ ⊢i (subst_ctx C A ---> ⊥) using i.
End FOL_helpers.
Lemma prf_prop_bott_iff {Σ : Signature} Γ AC:
Γ ⊢i ((subst_ctx AC patt_bott) <---> patt_bott)
using (
(ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)).
Lemma Prop_disj_left {Σ : Signature} (Γ : Theory) (ϕ₁ ϕ₂ ψ : Pattern) :
well_formed ϕ₁ →
well_formed ϕ₂ →
well_formed ψ →
Γ ⊢i (ϕ₁ or ϕ₂) ⋅ ψ ---> (ϕ₁ ⋅ ψ) or (ϕ₂ ⋅ ψ) using BasicReasoning.
Lemma Prop_disj_right {Σ : Signature} (Γ : Theory) (ϕ₁ ϕ₂ ψ : Pattern) :
well_formed ϕ₁ →
well_formed ϕ₂ →
well_formed ψ →
Γ ⊢i ψ ⋅ (ϕ₁ or ϕ₂) ---> (ψ ⋅ ϕ₁) or (ψ ⋅ ϕ₂) using BasicReasoning.
Lemma prf_prop_or_iff {Σ : Signature} Γ AC p q:
well_formed p →
well_formed q →
Γ ⊢i ((subst_ctx AC (p or q)) <---> ((subst_ctx AC p) or (subst_ctx AC q)))
using (
(ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)).
Lemma Singleton_ctx {Σ : Signature} (Γ : Theory) (C1 C2 : Application_context) (ϕ : Pattern) (x : evar) :
well_formed ϕ →
Γ ⊢i (! ((subst_ctx C1 (patt_free_evar x and ϕ)) and
(subst_ctx C2 (patt_free_evar x and (! ϕ)))))
using BasicReasoning.
Lemma Existence {Σ : Signature} (Γ : Theory) :
Γ ⊢i (ex , patt_bound_evar 0) using BasicReasoning.
Lemma Prop_ex_left {Σ : Signature} (Γ : Theory) (ϕ ψ : Pattern) :
well_formed (ex, ϕ) →
well_formed ψ →
Γ ⊢i (ex , ϕ) ⋅ ψ ---> ex , ϕ ⋅ ψ
using BasicReasoning.
Lemma Prop_ex_right {Σ : Signature} (Γ : Theory) (ϕ ψ : Pattern) :
well_formed (ex, ϕ) →
well_formed ψ →
Γ ⊢i ψ ⋅ (ex , ϕ) ---> ex , ψ ⋅ ϕ
using BasicReasoning.
Lemma prf_prop_ex_iff {Σ : Signature} Γ AC p x:
evar_is_fresh_in x (subst_ctx AC p) →
well_formed (patt_exists p) = true →
Γ ⊢i ((subst_ctx AC (patt_exists p)) <---> (exists_quantify x (subst_ctx AC (p^{evar: 0 ↦ x}))))
using (
{| pi_generalized_evars := {[x]};
pi_substituted_svars := ∅;
pi_uses_kt := false ;
pi_uses_advanced_kt := false ;
|}).
Add Search Blacklist "_elim".
Add Search Blacklist "_graph_rect".
Add Search Blacklist "_graph_mut".
Add Search Blacklist "FunctionalElimination_".
Section FOL_helpers.
Context {Σ : Signature}.
From MatchingLogic.ProofMode Require Export Reshaper FixPoint.
(*
Require Import wftactics2. *)
Import MatchingLogic.Logic.Notations.
Open Scope list_scope. (* needed for mlAssert, ++ *)
(* TODO: create error messages for these tactics *)
Ltac2 _callCompletedTransformedAndCast0
(t : constr) (transform : constr) (tac : constr → unit) :=
let tac' := (fun (t' : constr) ⇒
let tac'' := (fun (t'' : constr) ⇒
let tcast := open_constr:(@useGenericReasoning'' _ _ _ _ _ $t'') in
fillWithUnderscoresAndCall0 tac tcast []
) in
fillWithUnderscoresAndCall0 (fun t''' ⇒ tac'' t''') transform [t']
) in
fillWithUnderscoresAndCall0 tac' t []
.
Ltac2 _callCompletedTransformedAndCast
(twb : Std.constr_with_bindings) (transform : constr) (tac : constr → unit) :=
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
_callCompletedTransformedAndCast0 t_constr transform tac;
clear $t
.
Ltac2 do_mlApplyMetaGeneralized (twb : Std.constr_with_bindings) :=
Control.enter(fun () ⇒
_callCompletedTransformedAndCast twb constr:(@reshape_lhs_imp_to_and_forward) do_mlApplyMetaRaw ;
try_solve_pile_basic ();
try_wfa ();
ltac1:(rewrite [foldr patt_and _ _]/=)
)
.
Ltac2 Notation "mlApplyMetaGeneralized" t(seq(open_constr,with_bindings)) :=
do_mlApplyMetaGeneralized t
.
Tactic Notation "mlApplyMetaGeneralized" uconstr(t) :=
let f := ltac2:(t |- do_mlApplyMetaGeneralized ((Option.get (Ltac1.to_constr t)), Std.NoBindings)) in
f t
.
Ltac2 Set do_mlApplyMeta as old_do_mlApplyMeta := fun (twb : Std.constr_with_bindings) ⇒
orelse (fun () ⇒ old_do_mlApplyMeta twb) (fun _ ⇒ do_mlApplyMetaGeneralized twb)
.
#[local]
Example ex_mlApplyMetaGeneralized {Σ : Signature} Γ a b c d e f:
well_formed a →
well_formed b →
well_formed c →
well_formed d →
well_formed e →
well_formed f →
Γ ⊢ a ---> b ---> c ---> d ---> e ---> f →
Γ ⊢ (a and (b and (c and (d and e)))) ---> f.
#[local]
Example ex_mlApplyMetaGeneralized2 {Σ : Signature} Γ a b c d e f:
well_formed a →
well_formed b →
well_formed c →
well_formed d →
well_formed e →
well_formed f →
(∀ c', well_formed c' = true → Γ ⊢ a ---> b ---> c' ---> d ---> e ---> f) →
Γ ⊢ (a and (b and (c and (d and e)))) ---> f.
Lemma foldr_andb_init_true i l:
foldr andb i l = true → i = true.
Lemma foldr_andb_true_iff i l:
foldr andb i l = i && foldr andb true l.
Lemma MLGoal_weakenConclusionGen' {Σ : Signature} Γ l₁ l₂ name g' i
(x : Pattern) (xs : list Pattern)
:
∀ (r : ImpReshapeS g' (x::xs)),
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name ((untagPattern (irs_flattened _ _ r)))) :: l₂) ((foldr (patt_and) x xs)) i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name ((untagPattern (irs_flattened _ _ r)))) :: l₂) g' i.
Lemma MLGoal_weakenConclusionGen {Σ : Signature} Γ l₁ l₂ name g' i
(x : Pattern) (xs : list Pattern)
:
∀ (r : ImpReshapeS g' (x::xs)),
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name ((untagPattern (irs_flattened _ _ r)))) :: l₂)
(
match (rev xs) with
| [] ⇒ x
| yk::ys ⇒ (foldr (patt_and) yk (x::(rev ys)))
end
)
i →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name ((untagPattern (irs_flattened _ _ r)))) :: l₂) g' i.
(* TODO: Reformulate this in Ltac2 *)
Tactic Notation "_mlApplyBasic" constr(name') :=
_ensureProofMode;
_mlReshapeHypsByName name';
tryif apply MLGoal_weakenConclusion;
_mlReshapeHypsBack
then idtac
else fail "_mlApplyBasic: Hypothesis does not match the goal".
(* TODO: Reformulate this in Ltac2 *)
Tactic Notation "_mlApplyGen" constr(name') :=
_ensureProofMode;
_mlReshapeHypsByName name';
tryif apply MLGoal_weakenConclusionGen;
_mlReshapeHypsBack
then idtac
else fail "_mlApplyGen: Hypothesis does not match the goal".
#[local]
Example ex_mlApplyGeneralized {Σ : Signature} Γ a b c d e f g:
well_formed a →
well_formed b →
well_formed c →
well_formed d →
well_formed e →
well_formed f →
well_formed g →
Γ ⊢ ((a and (b and (c and (d and e)))) --->
(a ---> b ---> c ---> d ---> e ---> f) --->
(f ---> g) --->
g).
Tactic Notation "mlApply" constr(name') :=
(_mlApplyBasic name') || (_mlApplyGen name')
.
Section FOL_helpers.
Context {Σ : Signature}.
Lemma Prop_bott_left (Γ : Theory) (ϕ : Pattern) :
well_formed ϕ →
Γ ⊢i ⊥ ⋅ ϕ ---> ⊥ using BasicReasoning.
Lemma Prop_bott_right (Γ : Theory) (ϕ : Pattern) :
well_formed ϕ →
Γ ⊢i ϕ ⋅ ⊥ ---> ⊥ using BasicReasoning.
Arguments Prop_bott_left _ (_%_ml) _ : clear implicits.
Arguments Prop_bott_right _ (_%_ml) _ : clear implicits.
Lemma Prop_bot_ctx (Γ : Theory) (C : Application_context) :
Γ ⊢i ((subst_ctx C patt_bott) ---> patt_bott)
using (ExGen := ∅, SVSubst := ∅, KT := false, AKT := false).
Lemma Framing (Γ : Theory) (C : Application_context) (A B : Pattern) (i : ProofInfo)
{pile : ProofInfoLe
((ExGen := ∅, SVSubst := ∅, KT := false, AKT := false))
i
}
:
Γ ⊢i (A ---> B) using i →
Γ ⊢i ((subst_ctx C A) ---> (subst_ctx C B)) using i.
Lemma A_implies_not_not_A_ctx (Γ : Theory) (A : Pattern) (C : Application_context)
(i : ProofInfo) {pile : ProofInfoLe ((ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)) i}
:
well_formed A →
Γ ⊢i A using i →
Γ ⊢i (! (subst_ctx C ( !A ))) using i.
Lemma ctx_bot_prop (Γ : Theory) (C : Application_context) (A : Pattern)
(i : ProofInfo)
{pile : ProofInfoLe ((ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)) i}
:
well_formed A →
Γ ⊢i (A ---> ⊥) using i →
Γ ⊢i (subst_ctx C A ---> ⊥) using i.
End FOL_helpers.
Lemma prf_prop_bott_iff {Σ : Signature} Γ AC:
Γ ⊢i ((subst_ctx AC patt_bott) <---> patt_bott)
using (
(ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)).
Lemma Prop_disj_left {Σ : Signature} (Γ : Theory) (ϕ₁ ϕ₂ ψ : Pattern) :
well_formed ϕ₁ →
well_formed ϕ₂ →
well_formed ψ →
Γ ⊢i (ϕ₁ or ϕ₂) ⋅ ψ ---> (ϕ₁ ⋅ ψ) or (ϕ₂ ⋅ ψ) using BasicReasoning.
Lemma Prop_disj_right {Σ : Signature} (Γ : Theory) (ϕ₁ ϕ₂ ψ : Pattern) :
well_formed ϕ₁ →
well_formed ϕ₂ →
well_formed ψ →
Γ ⊢i ψ ⋅ (ϕ₁ or ϕ₂) ---> (ψ ⋅ ϕ₁) or (ψ ⋅ ϕ₂) using BasicReasoning.
Lemma prf_prop_or_iff {Σ : Signature} Γ AC p q:
well_formed p →
well_formed q →
Γ ⊢i ((subst_ctx AC (p or q)) <---> ((subst_ctx AC p) or (subst_ctx AC q)))
using (
(ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)).
Lemma Singleton_ctx {Σ : Signature} (Γ : Theory) (C1 C2 : Application_context) (ϕ : Pattern) (x : evar) :
well_formed ϕ →
Γ ⊢i (! ((subst_ctx C1 (patt_free_evar x and ϕ)) and
(subst_ctx C2 (patt_free_evar x and (! ϕ)))))
using BasicReasoning.
Lemma Existence {Σ : Signature} (Γ : Theory) :
Γ ⊢i (ex , patt_bound_evar 0) using BasicReasoning.
Lemma Prop_ex_left {Σ : Signature} (Γ : Theory) (ϕ ψ : Pattern) :
well_formed (ex, ϕ) →
well_formed ψ →
Γ ⊢i (ex , ϕ) ⋅ ψ ---> ex , ϕ ⋅ ψ
using BasicReasoning.
Lemma Prop_ex_right {Σ : Signature} (Γ : Theory) (ϕ ψ : Pattern) :
well_formed (ex, ϕ) →
well_formed ψ →
Γ ⊢i ψ ⋅ (ex , ϕ) ---> ex , ψ ⋅ ϕ
using BasicReasoning.
Lemma prf_prop_ex_iff {Σ : Signature} Γ AC p x:
evar_is_fresh_in x (subst_ctx AC p) →
well_formed (patt_exists p) = true →
Γ ⊢i ((subst_ctx AC (patt_exists p)) <---> (exists_quantify x (subst_ctx AC (p^{evar: 0 ↦ x}))))
using (
{| pi_generalized_evars := {[x]};
pi_substituted_svars := ∅;
pi_uses_kt := false ;
pi_uses_advanced_kt := false ;
|}).
Add Search Blacklist "_elim".
Add Search Blacklist "_graph_rect".
Add Search Blacklist "_graph_mut".
Add Search Blacklist "FunctionalElimination_".
Section FOL_helpers.
Context {Σ : Signature}.
NOTE: DO NOT REPLACE! The element variable in this function is
needed to substitute in such pattern context, which contain
arbitrary patterns, but the path to the element variable
is concrete. For example, in `⌈ E ⌉ ⋅ φ` the path to `E` does
not contain any ∃-s, thus no new variables need to be generated
for `mlRewrite`.
Fixpoint maximal_exists_depth_to (depth : nat) (E : evar) (ψ : Pattern) : nat :=
match ψ with
| patt_bott ⇒ 0
| patt_sym _ ⇒ 0
| patt_bound_evar _ ⇒ 0
| patt_bound_svar _ ⇒ 0
| patt_free_svar _ ⇒ 0
| patt_free_evar E' ⇒
match (decide (E' = E)) with
| left _ ⇒ depth
| right _ ⇒ 0
end
| patt_imp ψ₁ ψ₂
⇒ Nat.max
(maximal_exists_depth_to depth E ψ₁)
(maximal_exists_depth_to depth E ψ₂)
| patt_app ψ₁ ψ₂
⇒ Nat.max
(maximal_exists_depth_to depth E ψ₁)
(maximal_exists_depth_to depth E ψ₂)
| patt_exists ψ' ⇒ maximal_exists_depth_to (S depth) E ψ'
| patt_mu ψ' ⇒ maximal_exists_depth_to depth E ψ'
end.
Lemma maximal_exists_depth_to_0 E ψ depth:
E ∉ free_evars ψ →
maximal_exists_depth_to depth E ψ = 0.
Lemma maximal_exists_depth_to_S E ψ depth:
E ∈ free_evars ψ →
maximal_exists_depth_to (S depth) E ψ
= S (maximal_exists_depth_to depth E ψ).
Lemma evar_open_exists_depth φ depth x e : ∀ dbi,
x ≠ e →
maximal_exists_depth_to depth x φ^{evar: dbi ↦ e} = maximal_exists_depth_to depth x φ.
Lemma svar_open_exists_depth φ depth x X : ∀ dbi,
maximal_exists_depth_to depth x φ^{svar: dbi ↦ X} = maximal_exists_depth_to depth x φ.
Lemma svar_fresh_seq_max (SvS : SVarSet) (n1 n2 : nat) :
(@list_to_set svar SVarSet _ _ _ (svar_fresh_seq SvS n1)) ⊆ (list_to_set (svar_fresh_seq SvS (n1 `max` n2))).
Lemma congruence_ex Γ E ψ x p q gpi kt evs svs
(HxneqE : x ≠ E)
(wfψ : well_formed (ex , ψ))
(wfp : well_formed p)
(wfq : well_formed q)
(Heqx : x ∉ free_evars ψ ∪ free_evars p ∪ free_evars q)
(Heqx2 : x ∈ evs)
(pile: ProofInfoLe (ExGen := evs, SVSubst := svs, KT := kt, AKT := false) gpi)
(IH: Γ ⊢i ψ^{evar: 0 ↦ x}^[[evar: E ↦ p]] <---> ψ^{evar: 0 ↦ x}^[[evar: E ↦ q]]
using gpi) :
(Γ ⊢i (ex , ψ^[[evar: E ↦ p]]) <---> (ex , ψ^[[evar: E ↦ q]]) using gpi).
End FOL_helpers.
Ltac pi_exact H :=
lazymatch type of H with
| ?H' ⇒
lazymatch goal with
| [|- ?g] ⇒
(cut (H' = g);
[(let H0 := fresh "H0" in intros H0; rewrite -H0; exact H)|
(repeat f_equal; try reflexivity; try apply proof_irrel)])
end
end.
Ltac pi_assumption :=
match goal with
| [H : _ |- _] ⇒ pi_exact H
end.
Ltac pi_set_solver := set_solver by (try pi_assumption).
Section FOL_helpers.
Context {Σ : Signature}.
Lemma congruence_app1 Γ ψ1 ψ2 p q E i
(wfψ1: well_formed ψ1)
(wfψ2: well_formed ψ2)
(wfp: well_formed p)
(wfq: well_formed q)
(pf₁: Γ ⊢i ψ1^[[evar: E ↦ p]] ---> ψ1^[[evar: E ↦ q]] using i)
(pf₂: Γ ⊢i ψ2^[[evar: E ↦ p]] ---> ψ2^[[evar: E ↦ q]] using i)
:
(Γ ⊢i (ψ1^[[evar: E ↦ p]]) ⋅ (ψ2^[[evar: E ↦ p]]) ---> (ψ1^[[evar: E ↦ q]]) ⋅ (ψ2^[[evar: E ↦ q]]) using i).
Lemma congruence_app Γ ψ1 ψ2 p q E i
(wfψ1: well_formed ψ1)
(wfψ2: well_formed ψ2)
(wfp: well_formed p)
(wfq: well_formed q)
(pf₁: Γ ⊢i ψ1^[[evar: E ↦ p]] <---> ψ1^[[evar: E ↦ q]] using i)
(pf₂: Γ ⊢i ψ2^[[evar: E ↦ p]] <---> ψ2^[[evar: E ↦ q]] using i)
:
(Γ ⊢i (ψ1^[[evar: E ↦ p]]) ⋅ (ψ2^[[evar: E ↦ p]]) <---> (ψ1^[[evar: E ↦ q]]) ⋅ (ψ2^[[evar: E ↦ q]]) using i).
Lemma count_evar_occurrences_evar_replace φ x y :
x ∉ free_evars φ →
count_evar_occurrences x φ^[[evar:y↦patt_free_evar x]] =
count_evar_occurrences y φ.
Lemma eq_prf_equiv_congruence
(sz : nat)
Γ p q evs svs
(wfp : well_formed p)
(wfq : well_formed q)
E ψ edepth sdepth
(Hsz: pat_size ψ ≤ sz)
(wfψ : well_formed ψ)
(gpi : ProofInfo)
match ψ with
| patt_bott ⇒ 0
| patt_sym _ ⇒ 0
| patt_bound_evar _ ⇒ 0
| patt_bound_svar _ ⇒ 0
| patt_free_svar _ ⇒ 0
| patt_free_evar E' ⇒
match (decide (E' = E)) with
| left _ ⇒ depth
| right _ ⇒ 0
end
| patt_imp ψ₁ ψ₂
⇒ Nat.max
(maximal_exists_depth_to depth E ψ₁)
(maximal_exists_depth_to depth E ψ₂)
| patt_app ψ₁ ψ₂
⇒ Nat.max
(maximal_exists_depth_to depth E ψ₁)
(maximal_exists_depth_to depth E ψ₂)
| patt_exists ψ' ⇒ maximal_exists_depth_to (S depth) E ψ'
| patt_mu ψ' ⇒ maximal_exists_depth_to depth E ψ'
end.
Lemma maximal_exists_depth_to_0 E ψ depth:
E ∉ free_evars ψ →
maximal_exists_depth_to depth E ψ = 0.
Lemma maximal_exists_depth_to_S E ψ depth:
E ∈ free_evars ψ →
maximal_exists_depth_to (S depth) E ψ
= S (maximal_exists_depth_to depth E ψ).
Lemma evar_open_exists_depth φ depth x e : ∀ dbi,
x ≠ e →
maximal_exists_depth_to depth x φ^{evar: dbi ↦ e} = maximal_exists_depth_to depth x φ.
Lemma svar_open_exists_depth φ depth x X : ∀ dbi,
maximal_exists_depth_to depth x φ^{svar: dbi ↦ X} = maximal_exists_depth_to depth x φ.
Lemma svar_fresh_seq_max (SvS : SVarSet) (n1 n2 : nat) :
(@list_to_set svar SVarSet _ _ _ (svar_fresh_seq SvS n1)) ⊆ (list_to_set (svar_fresh_seq SvS (n1 `max` n2))).
Lemma congruence_ex Γ E ψ x p q gpi kt evs svs
(HxneqE : x ≠ E)
(wfψ : well_formed (ex , ψ))
(wfp : well_formed p)
(wfq : well_formed q)
(Heqx : x ∉ free_evars ψ ∪ free_evars p ∪ free_evars q)
(Heqx2 : x ∈ evs)
(pile: ProofInfoLe (ExGen := evs, SVSubst := svs, KT := kt, AKT := false) gpi)
(IH: Γ ⊢i ψ^{evar: 0 ↦ x}^[[evar: E ↦ p]] <---> ψ^{evar: 0 ↦ x}^[[evar: E ↦ q]]
using gpi) :
(Γ ⊢i (ex , ψ^[[evar: E ↦ p]]) <---> (ex , ψ^[[evar: E ↦ q]]) using gpi).
End FOL_helpers.
Ltac pi_exact H :=
lazymatch type of H with
| ?H' ⇒
lazymatch goal with
| [|- ?g] ⇒
(cut (H' = g);
[(let H0 := fresh "H0" in intros H0; rewrite -H0; exact H)|
(repeat f_equal; try reflexivity; try apply proof_irrel)])
end
end.
Ltac pi_assumption :=
match goal with
| [H : _ |- _] ⇒ pi_exact H
end.
Ltac pi_set_solver := set_solver by (try pi_assumption).
Section FOL_helpers.
Context {Σ : Signature}.
Lemma congruence_app1 Γ ψ1 ψ2 p q E i
(wfψ1: well_formed ψ1)
(wfψ2: well_formed ψ2)
(wfp: well_formed p)
(wfq: well_formed q)
(pf₁: Γ ⊢i ψ1^[[evar: E ↦ p]] ---> ψ1^[[evar: E ↦ q]] using i)
(pf₂: Γ ⊢i ψ2^[[evar: E ↦ p]] ---> ψ2^[[evar: E ↦ q]] using i)
:
(Γ ⊢i (ψ1^[[evar: E ↦ p]]) ⋅ (ψ2^[[evar: E ↦ p]]) ---> (ψ1^[[evar: E ↦ q]]) ⋅ (ψ2^[[evar: E ↦ q]]) using i).
Lemma congruence_app Γ ψ1 ψ2 p q E i
(wfψ1: well_formed ψ1)
(wfψ2: well_formed ψ2)
(wfp: well_formed p)
(wfq: well_formed q)
(pf₁: Γ ⊢i ψ1^[[evar: E ↦ p]] <---> ψ1^[[evar: E ↦ q]] using i)
(pf₂: Γ ⊢i ψ2^[[evar: E ↦ p]] <---> ψ2^[[evar: E ↦ q]] using i)
:
(Γ ⊢i (ψ1^[[evar: E ↦ p]]) ⋅ (ψ2^[[evar: E ↦ p]]) <---> (ψ1^[[evar: E ↦ q]]) ⋅ (ψ2^[[evar: E ↦ q]]) using i).
Lemma count_evar_occurrences_evar_replace φ x y :
x ∉ free_evars φ →
count_evar_occurrences x φ^[[evar:y↦patt_free_evar x]] =
count_evar_occurrences y φ.
Lemma eq_prf_equiv_congruence
(sz : nat)
Γ p q evs svs
(wfp : well_formed p)
(wfq : well_formed q)
E ψ edepth sdepth
(Hsz: pat_size ψ ≤ sz)
(wfψ : well_formed ψ)
(gpi : ProofInfo)
We need to do a number of Ex_Gen (and Substitution) steps
in the proof, thus we need at least as many fresh variables
as ∃-s (and μ-s) are in ψ. These should also be included in gpi.
Actually, we do not need that many variables always, then
depth of ∃-s should only be considered in the paths where
E is present. For simplicity (and the fact that we have
infinitely many fresh variables), we chose not to use that
approach
el
(Hel1 : fresh_evars el (free_evars ψ ∪ free_evars p ∪ free_evars q ∪ {[E]}))
(Hel2 : length el ≥ maximal_exists_depth_to edepth E ψ)
(Hel3 : ∀ x, x ∈ el → x ∈ evs)
sl
(Hsl1 : fresh_svars sl (free_svars ψ ∪ free_svars p ∪ free_svars q))
(Hsl2 : length sl ≥ maximal_mu_depth_to sdepth E ψ)
(Hsl3 : ∀ X, X ∈ sl → X ∈ svs)
(pile: ProofInfoLe
(ExGen := evs,
SVSubst := svs,
KT := mu_in_evar_path E ψ sdepth,
AKT := mu_in_evar_path E ψ sdepth (* TODO relax*)) gpi)
(pf : Γ ⊢i (p <---> q) using ( gpi)) :
Γ ⊢i (((ψ^[[evar: E ↦ p]]) <---> (ψ^[[evar: E ↦ q]]))) using ( gpi).
(* Correctness of evar_fresh_seq *)
Lemma evar_fresh_seq_correct n s:
fresh_evars (evar_fresh_seq s n) s.
(* Correctness of svar_fresh_seq *)
Lemma svar_fresh_seq_correct n s:
fresh_svars (svar_fresh_seq s n) s.
Lemma evar_fresh_seq_length l n:
length (evar_fresh_seq l n) = n.
Lemma svar_fresh_seq_length l n:
length (svar_fresh_seq l n) = n.
Lemma prf_equiv_congruence Γ p q C
(gpi : ProofInfo)
(wfp : well_formed p = true)
(wfq : well_formed q = true)
(wfC: PC_wf C)
(pile : ProofInfoLe
(ExGen := list_to_set (evar_fresh_seq (free_evars (pcPattern C) ∪ free_evars p ∪ free_evars q ∪ {[pcEvar C]}) (maximal_exists_depth_to 0 (pcEvar C) (pcPattern C))),
SVSubst := list_to_set (svar_fresh_seq (free_svars (pcPattern C) ∪ free_svars p ∪ free_svars q) (maximal_mu_depth_to 0 (pcEvar C) (pcPattern C))),
KT := mu_in_evar_path (pcEvar C) (pcPattern C) 0,
AKT := mu_in_evar_path (pcEvar C) (pcPattern C) 0 (* TODO: relax*)
)
gpi
) :
Γ ⊢i (p <---> q) using ( gpi) →
Γ ⊢i (((emplace C p) <---> (emplace C q))) using ( gpi).
End FOL_helpers.
Lemma collapse_free_evar_subst {Σ : Signature} φ ψ x y:
y ∉ free_evars φ →
φ^[[evar: x ↦ patt_free_evar y]]^[[evar: y ↦ ψ]] =
φ^[[evar: x ↦ ψ]].
Lemma fresh_foldr_is_context {Σ : Signature} l C p:
pcEvar C ∉ free_evars_of_list l →
foldr patt_imp (emplace C p) l =
emplace
{|pcEvar := pcEvar C;
pcPattern := foldr patt_imp (pcPattern C) l |} p.
(Hel1 : fresh_evars el (free_evars ψ ∪ free_evars p ∪ free_evars q ∪ {[E]}))
(Hel2 : length el ≥ maximal_exists_depth_to edepth E ψ)
(Hel3 : ∀ x, x ∈ el → x ∈ evs)
sl
(Hsl1 : fresh_svars sl (free_svars ψ ∪ free_svars p ∪ free_svars q))
(Hsl2 : length sl ≥ maximal_mu_depth_to sdepth E ψ)
(Hsl3 : ∀ X, X ∈ sl → X ∈ svs)
(pile: ProofInfoLe
(ExGen := evs,
SVSubst := svs,
KT := mu_in_evar_path E ψ sdepth,
AKT := mu_in_evar_path E ψ sdepth (* TODO relax*)) gpi)
(pf : Γ ⊢i (p <---> q) using ( gpi)) :
Γ ⊢i (((ψ^[[evar: E ↦ p]]) <---> (ψ^[[evar: E ↦ q]]))) using ( gpi).
(* Correctness of evar_fresh_seq *)
Lemma evar_fresh_seq_correct n s:
fresh_evars (evar_fresh_seq s n) s.
(* Correctness of svar_fresh_seq *)
Lemma svar_fresh_seq_correct n s:
fresh_svars (svar_fresh_seq s n) s.
Lemma evar_fresh_seq_length l n:
length (evar_fresh_seq l n) = n.
Lemma svar_fresh_seq_length l n:
length (svar_fresh_seq l n) = n.
Lemma prf_equiv_congruence Γ p q C
(gpi : ProofInfo)
(wfp : well_formed p = true)
(wfq : well_formed q = true)
(wfC: PC_wf C)
(pile : ProofInfoLe
(ExGen := list_to_set (evar_fresh_seq (free_evars (pcPattern C) ∪ free_evars p ∪ free_evars q ∪ {[pcEvar C]}) (maximal_exists_depth_to 0 (pcEvar C) (pcPattern C))),
SVSubst := list_to_set (svar_fresh_seq (free_svars (pcPattern C) ∪ free_svars p ∪ free_svars q) (maximal_mu_depth_to 0 (pcEvar C) (pcPattern C))),
KT := mu_in_evar_path (pcEvar C) (pcPattern C) 0,
AKT := mu_in_evar_path (pcEvar C) (pcPattern C) 0 (* TODO: relax*)
)
gpi
) :
Γ ⊢i (p <---> q) using ( gpi) →
Γ ⊢i (((emplace C p) <---> (emplace C q))) using ( gpi).
End FOL_helpers.
Lemma collapse_free_evar_subst {Σ : Signature} φ ψ x y:
y ∉ free_evars φ →
φ^[[evar: x ↦ patt_free_evar y]]^[[evar: y ↦ ψ]] =
φ^[[evar: x ↦ ψ]].
Lemma fresh_foldr_is_context {Σ : Signature} l C p:
pcEvar C ∉ free_evars_of_list l →
foldr patt_imp (emplace C p) l =
emplace
{|pcEvar := pcEvar C;
pcPattern := foldr patt_imp (pcPattern C) l |} p.
NOTE: the following lemmas are very specific for prf_equiv_congruence_iter
Lemma maximal_exists_depth_foldr_notin {Σ : Signature} l ψ x edepth:
x ∉ free_evars_of_list l →
maximal_exists_depth_to edepth x (foldr patt_imp ψ l) =
maximal_exists_depth_to edepth x ψ.
Lemma maximal_mu_depth_foldr_notin {Σ : Signature} l ψ x edepth:
x ∉ free_evars_of_list l →
maximal_mu_depth_to edepth x (foldr patt_imp ψ l) =
maximal_mu_depth_to edepth x ψ.
(* NOTE: This version of the iterated congruence lemma is proved by induction.
There is a way, to prove this lemma without induction (see
`TEST_proofmode_proof_size.v`), but the generated proof term becomes
much more larger (2-3 times larger than the induction-based).
This is because the proof of the congruence lemma is more complex
for bigger contexts. *)
Lemma prf_equiv_congruence_iter {Σ : Signature} (Γ : Theory) (p q : Pattern) (C : PatternCtx) l
(wfp : well_formed p)
(wfq : well_formed q)
(wfC : PC_wf C)
(gpi : ProofInfo)
(pile : ProofInfoLe
(ExGen := list_to_set (evar_fresh_seq (free_evars (pcPattern C) ∪ free_evars p ∪ free_evars q ∪ {[pcEvar C]}) (maximal_exists_depth_to 0 (pcEvar C) (pcPattern C))),
SVSubst := list_to_set (svar_fresh_seq (free_svars (pcPattern C) ∪ free_svars p ∪ free_svars q) (maximal_mu_depth_to 0 (pcEvar C) (pcPattern C))),
KT := mu_in_evar_path (pcEvar C) (pcPattern C) 0,
AKT := mu_in_evar_path (pcEvar C) (pcPattern C) 0 (* TODO relax *)
)
( gpi)
):
Pattern.wf l →
Γ ⊢i p <---> q using ( gpi) →
Γ ⊢i (foldr patt_imp (emplace C p) l) <---> (foldr patt_imp (emplace C q) l) using ( gpi).
Lemma extract_wfp {Σ : Signature} (Γ : Theory) (p q : Pattern) (i : ProofInfo):
Γ ⊢i p <---> q using i →
well_formed p.
Lemma extract_wfq {Σ : Signature} (Γ : Theory) (p q : Pattern) (i : ProofInfo):
Γ ⊢i p <---> q using i →
well_formed q.
Lemma MLGoal_rewriteIff
{Σ : Signature} (Γ : Theory) (p q : Pattern) (C : PatternCtx) l (gpi : ProofInfo)
(wfC : PC_wf C)
(pf : Γ ⊢i p <---> q using ( gpi)) :
mkMLGoal Σ Γ l (emplace C q) ( gpi) →
(ProofInfoLe
(ExGen := list_to_set (evar_fresh_seq (free_evars (pcPattern C) ∪ free_evars p ∪ free_evars q ∪ {[pcEvar C]}) (maximal_exists_depth_to 0 (pcEvar C) (pcPattern C))),
SVSubst := list_to_set (svar_fresh_seq (free_svars (pcPattern C) ∪
free_svars p ∪ free_svars q) (maximal_mu_depth_to 0 (pcEvar C) (pcPattern C))),
KT := mu_in_evar_path (pcEvar C) (pcPattern C) 0,
AKT := mu_in_evar_path (pcEvar C) (pcPattern C) 0 (* TODO: relax*)
)
gpi) →
mkMLGoal Σ Γ l (emplace C p) ( gpi).
Ltac2 mutable ml_debug_rewrite := false.
Ltac2 for_nth_match :=
fun (n : int) (a : constr) (phi : constr) (cont : Pattern.context → unit) ⇒
try (
if ml_debug_rewrite then
Message.print (
Message.concat
(Message.of_string "Trying to match ")
(Message.of_constr a)
)
else ();
let curr : int ref := {contents := 0} in
match! phi with
| context ctx [ ?x ]
⇒ if ml_debug_rewrite then
Message.print (
Message.concat
(Message.of_string " against ")
(Message.of_constr x)
)
else ();
(* lazy_match! Constr.type x with (* Optimisation, but it does not help much *)
| Pattern => *)
(if Constr.equal x a then
if ml_debug_rewrite then
Message.print (Message.of_string "Success.")
else () ;
curr.(contents) := Int.add 1 (curr.(contents)) ;
if (Int.equal (curr.(contents)) n) then
cont ctx
else fail
else fail)
end
); ()
.
Local Ltac reduce_free_evar_subst_step_2 star :=
lazymatch goal with
| [ |- context ctx [?p^[[evar: star ↦ ?q]] ] ]
⇒
progress rewrite → (@free_evar_subst_no_occurrence _ star p q) by (
subst star;
eapply evar_is_fresh_in_richer';
[|apply set_evar_fresh_is_fresh'];
simpl; clear; set_solver
)
end.
Local Ltac reduce_free_evar_subst_2 star :=
(* unfold free_evar_subst; *)
repeat (reduce_free_evar_subst_step_2 star).
Local Tactic Notation "solve_fresh_contradictions_2'" constr(star) constr(x) constr(h) :=
let hcontra := fresh "Hcontra" in
assert (hcontra: x ≠ star) by (subst star; unfold fresh_evar,evar_fresh_s; try clear h; simpl; solve_fresh_neq);
rewrite → h in hcontra;
contradiction.
Local Ltac solve_fresh_contradictions_2 star :=
unfold fresh_evar; simpl;
match goal with
| h: ?x = star |- _ ⇒
let hprime := fresh "hprime" in
pose proof (hprime := eq_sym h);
solve_fresh_contradictions_2' star x hprime
| h: star = ?x |- _
⇒ solve_fresh_contradictions_2' star x h
end.
Local Ltac clear_obvious_equalities_2 :=
repeat (
match goal with
| [ h: ?x = ?x |- _ ] ⇒ clear h
end
).
Ltac simplify_emplace_2 star :=
unfold emplace;
(* unfold free_evar_subst; *)
cbn;
repeat break_match_goal;
clear_obvious_equalities_2; try contradiction;
try (solve_fresh_contradictions_2 star);
(* repeat (rewrite nest_ex_aux_0); *)
reduce_free_evar_subst_2 star.
(* Returns nth matching logic context C (of type PatternCtx) such that
emplace C a = phi.
*)
(* Ltac simplify_pile_side_condition_helper star :=
subst star;
unfold fresh_evar,evar_fresh_s;
eapply evar_is_fresh_in_richer';
|apply set_evar_fresh_is_fresh';
clear; simpl; set_solver. *)
Ltac rewrite_0_depths star :=
unfold mu_in_evar_path; cbn;
repeat rewrite (maximal_exists_depth_to_0 star);
repeat rewrite (maximal_mu_depth_to_0 star);
repeat match goal with
| [ |- context ctx [decide (star = star)] ] ⇒
destruct (decide (star = star)); try congruence
| [ |- context ctx [decide (?x = star)] ] ⇒
destruct (decide (x = star)); try congruence
| [ |- context ctx [decide (star = ?x)] ] ⇒
destruct (decide (star = x)); try congruence
| _ ⇒ idtac
end;
cbn.
Ltac try_solve_complex_pile star :=
try apply pile_any;
simplify_emplace_2 star;
(rewrite_0_depths star);
match goal with
| |- star ∉ free_evars _ ⇒ subst star; solve_fresh
| |- ProofInfoLe _ _ ⇒ try_solve_pile
end.
Ltac2 Type HeatResult := {
star_ident : ident ;
star_eq : ident ;
pc : constr ;
ctx : Pattern.context ;
ctx_pat : constr ;
equality : ident ;
}.
NOTE: with the new MLGoal_rewriteIff, we also need the variables
used in the list of hypotheses (l) for the fresh name
generation.
Ltac2 heat :=
fun (n : int) (a : constr) (phi : constr) : HeatResult ⇒
let found : (Pattern.context option) ref := { contents := None } in
for_nth_match n a phi
(fun ctx ⇒
found.(contents) := Some ctx; ()
);
match found.(contents) with
| None ⇒ throw_pm_exn (Message.concat (Message.of_string "heat: could not find match for pattern: '")
(Message.concat (Message.of_constr a)
(Message.concat (Message.of_string "' inside '")
(Message.concat (Message.of_constr phi)
(Message.concat (Message.of_string "' for occurrence ")
(Message.of_int n)
)
)
)
)
)
| Some ctx
⇒ (
let fr := constr:(fresh_evar $phi) in
let star_ident := Fresh.in_goal ident:(star) in
let star_eq := Fresh.in_goal ident:(star_eq) in
(*set (fr);*)
remember $fr as $star_ident eqn:star_eq;
let star_hyp := Control.hyp star_ident in
let ctxpat := Pattern.instantiate ctx constr:(patt_free_evar $star_hyp) in
let pc := constr:((@Build_PatternCtx _ $star_hyp $ctxpat)) in
let heq1 := Fresh.in_goal ident:(heq1) in
assert(heq1 : ($phi = (@emplace _ $pc $a)))
> [ abstract(
(* TODO: this is slow for bigger patterns *)
(ltac1:(star |- simplify_emplace_2 star) (Ltac1.of_ident star_ident);
reflexivity
))
| ()
];
{ star_ident := star_ident; star_eq := star_eq; pc := pc; ctx := ctx; ctx_pat := ctxpat; equality := heq1 }
)
end
.
Lemma cast_proof_ml_goal {Σ : Signature} Γ hyps goal goal' (e : goal = goal') (i : ProofInfo):
mkMLGoal Σ Γ hyps goal i →
mkMLGoal Σ Γ hyps goal' i .
Ltac2 mlRewrite (hiff : constr) (atn : int) :=
let thiff := Constr.type hiff in
(* we have to unfold derives otherwise this might not match *)
lazy_match! (eval unfold derives in $thiff) with
| _ ⊢i (?a <---> ?a') using _
⇒
unfold AnyReasoning;
lazy_match! goal with
| [ |- of_MLGoal (@mkMLGoal ?sgm ?g ?l ?p ( ?gpi))]
⇒
let hr : HeatResult := heat atn a p in
if ml_debug_rewrite then
Message.print (Message.concat (Message.of_string "Heating finished: ") (Message.of_constr (hr.(ctx_pat))))
else () ;
let heq := (* Control.hyp *) (hr.(equality)) in
let pc := (hr.(pc)) in
(* let var := (hr.(star_ident)) in
let ctx_p := (hr.(ctx_pat)) in *)
eapply (@cast_proof_ml_goal _ $g) with (goal := emplace $pc $a) >
[ ltac1:(heq |- rewrite [left in _ = left] heq; reflexivity) (Ltac1.of_ident heq) | ()];
Std.clear [hr.(equality)];
let wfC := Fresh.in_goal ident:(wfC) in
assert (wfC : PC_wf $pc = true) > [ ltac1:(unfold PC_wf; simpl; wf_auto2); Control.shelve () | ()] ;
let wfCpf := Control.hyp wfC in
Control.plus (fun () ⇒
apply (@MLGoal_rewriteIff $sgm $g _ _ $pc $l $gpi $wfCpf $hiff) >
[
(lazy_match! goal with
| [ |- of_MLGoal (@mkMLGoal ?_sgm ?g ?_l ?p _)]
⇒
let heq2 := Fresh.in_goal ident:(heq2) in
let plugged := Pattern.instantiate (hr.(ctx)) a' in
assert(heq2: ($p = $plugged))
> [
(* TODO: this is slow for bigger patterns *)
abstract (ltac1:(star |- simplify_emplace_2 star) (Ltac1.of_ident (hr.(star_ident)));
reflexivity
)
| ()
];
let heq2_pf := Control.hyp heq2 in
eapply (@cast_proof_ml_goal _ $g) >
[ rewrite $heq2_pf; reflexivity | ()];
Std.clear [wfC; heq2 ; (hr.(star_ident)); (hr.(star_eq))]
end)
| (ltac1:(star |- try_solve_complex_pile star) (Ltac1.of_ident (hr.(star_ident))))
]
)
(fun _ ⇒ throw_pm_exn (Message.concat (Message.of_string "mlRewrite: failed when rewriting '")
(Message.concat (Message.of_constr (a))
(Message.concat (Message.of_string "' to/from '")
(Message.concat (Message.of_constr (a'))
(Message.concat (Message.of_string "' in context ")
(Message.of_constr (pc))
)
)
)
)
)
)
| [ |- _] ⇒ throw_pm_exn_with_goal "mlRewrite: not in proof mode "
end
| ?x ⇒ throw_pm_exn (Message.concat (Message.of_string "mlRewrite: Given hypothesis is not an equivalence: ") (Message.of_constr x))
end.
Ltac2 rec constr_to_int (x : constr) : int :=
match! x with
| 0 ⇒ 0
| (S ?x') ⇒ Int.add 1 (constr_to_int x')
end.
Tactic Notation "mlRewrite" constr(Hiff) "at" constr(atn) :=
_ensureProofMode;
(let ff := ltac2:(hiff atn |-
mlRewrite
(Option.get (Ltac1.to_constr(hiff)))
(constr_to_int (Option.get (Ltac1.to_constr(atn))))
) in
ff Hiff atn);
fold AnyReasoning.
Lemma pf_iff_equiv_sym_meta {Σ : Signature} Γ A B i :
Γ ⊢i (A <---> B) using i →
Γ ⊢i (B <---> A) using i.
Tactic Notation "mlRewrite" "->" constr(Hiff) "at" constr(atn) :=
mlRewrite Hiff at atn.
Tactic Notation "mlRewrite" "<-" constr(Hiff) "at" constr(atn) :=
mlRewrite (@pf_iff_equiv_sym_meta _ _ _ _ _ Hiff) at atn.
Local Example ex_prf_rewrite_equiv_1 {Σ : Signature} Γ a a':
well_formed a →
well_formed a' →
Γ ⊢ a <---> a' →
Γ ⊢ a' →
Γ ⊢ a.
Local Example ex_prf_rewrite_equiv_foldl {Σ : Signature} Γ a a' l:
well_formed a →
well_formed a' →
Pattern.wf l →
Γ ⊢ a <---> a' →
Γ ⊢ foldr patt_imp a' l →
Γ ⊢ foldr patt_imp a l.
Local Example ex_prf_rewrite_equiv_2 {Σ : Signature} Γ a a' b x y z:
well_formed a →
well_formed a' →
well_formed (ex, b) →
Γ ⊢ a <---> a' →
Γ ⊢i (ex, ((patt_free_evar y) ---> (patt_free_evar z) ---> a ⋅ a ⋅ b ⋅ a ---> (patt_free_evar x)))
<---> (ex, ((patt_free_evar y) ---> (patt_free_evar z) ---> a ⋅ a' ⋅ b ⋅ a' ---> (patt_free_evar x)))
using AnyReasoning.
(* TODO: de-duplicate the code *)
Ltac2 rec convertToNNF_rewrite_pat := fun (ctx : constr) (p : constr) (i : constr) : unit ⇒
lazy_match! p with
| (! ! ?x) ⇒ (
let h' := Fresh.in_goal ident:(H) in
assert ($h' := (@not_not_eq _ $ctx $x ltac2:(wf_auto2 ())));
apply (@useBasicReasoning _ _ _ $i) in $h';
let h_constr := Control.hyp h' in
repeat (mlRewrite h_constr 1);
try (clear h');
convertToNNF_rewrite_pat ctx x i
)
| patt_not (patt_and ?x ?y) ⇒ (
let h' := Fresh.in_goal ident:(H) in
assert ($h' := (@deMorgan_nand _ $ctx $x $y ltac:(wf_auto2) ltac:(wf_auto2)));
apply (@useBasicReasoning _ _ _ $i) in $h';
let h_constr := Control.hyp h' in
repeat (mlRewrite h_constr 1);
try (clear h');
convertToNNF_rewrite_pat ctx constr:(!$x or !$y) i
)
| patt_not (patt_or ?x ?y) ⇒ (
let h' := Fresh.in_goal ident:(H) in
assert ($h' := (@deMorgan_nor _ $ctx $x $y ltac:(wf_auto2) ltac:(wf_auto2)));
apply (@useBasicReasoning _ _ _ $i) in $h';
let h_constr := Control.hyp h' in
repeat (mlRewrite h_constr 1);
try (clear h');
convertToNNF_rewrite_pat ctx constr:(!$x and !$y) i
)
| patt_not (?x ---> ?y) ⇒ (
let h' := Fresh.in_goal ident:(H) in
assert ($h' := (@nimpl_eq_and _ $ctx $x $y ltac:(wf_auto2) ltac:(wf_auto2)));
apply (@useBasicReasoning _ _ _ $i) in $h';
let h_constr := Control.hyp h' in
repeat (mlRewrite h_constr 1);
try (clear h');
convertToNNF_rewrite_pat ctx constr:($x and !$y) i
)
| (?x ---> ?y) ⇒ (
let h' := Fresh.in_goal ident:(H) in
assert ($h' := (@impl_eq_or _ $ctx $x $y ltac:(wf_auto2) ltac:(wf_auto2)));
apply (@useBasicReasoning _ _ _ $i) in $h';
let h_constr := Control.hyp h' in
repeat (mlRewrite h_constr 1);
try (clear h');
convertToNNF_rewrite_pat ctx constr:(!$x or $y) i
)
| patt_and ?x ?y ⇒ convertToNNF_rewrite_pat ctx x i; convertToNNF_rewrite_pat ctx y i
| patt_or ?x ?y ⇒ convertToNNF_rewrite_pat ctx x i; convertToNNF_rewrite_pat ctx y i
| _ ⇒ ()
end
.
Ltac2 toNNF () :=
repeat (do_mlRevertLast ());
lazy_match! goal with
| [ |- @of_MLGoal ?sgm (@mkMLGoal ?sgm ?ctx ?_ll ?g ?i) ]
⇒
do_mlApplyMetaRaw constr:(@useBasicReasoning _ _ _ $i (@not_not_elim $sgm $ctx $g ltac2:(wf_auto2 ())));
convertToNNF_rewrite_pat ctx constr:(!$g) i
end
.
Ltac toNNF := ltac2:(toNNF ()).
#[local] Example test_toNNF {Σ : Signature} Γ a b :
well_formed a →
well_formed b →
Γ ⊢i ( (b and (a or b) and !b and ( a or a) and a) ---> ⊥)
using BasicReasoning.
#[local]
Ltac rfindContradictionTo a ll k :=
match ll with
| ((mkNH _ ?name (! a)) :: ?m) ⇒
mlApply name; mlExactn k
| ((mkNH _ _ _) :: ?m) ⇒
rfindContradictionTo a m k
| _ ⇒ fail
end.
#[local]
Ltac findContradiction l k:=
match l with
| ((mkNH _ _ ?a) :: ?m) ⇒
match goal with
| [ |- @of_MLGoal ?Sgm (@mkMLGoal ?Sgm ?Ctx ?ll ?g ?i) ]
⇒
try rfindContradictionTo a ll k;
let kk := eval compute in ( k + 1 ) in
(findContradiction m kk)
end
| _ ⇒ fail
end.
#[local]
Ltac findContradiction_start :=
match goal with
| [ |- @of_MLGoal ?Sgm (@mkMLGoal ?Sgm ?Ctx ?l ?g ?i) ]
⇒
match goal with
| [ |- @of_MLGoal ?Sgm (@mkMLGoal ?Sgm ?Ctx ?l ?g ?i) ]
⇒
findContradiction l 0
end
end.
#[local]
Ltac breakHyps l :=
match l with
| ((mkNH _ ?name (?x and ?y)) :: ?m) ⇒
mlDestructAnd name
| ((mkNH _ ?name (?x or ?y)) :: ?m) ⇒
mlDestructOr name
| ((mkNH _ ?name ?x) :: ?m) ⇒
breakHyps m
end.
#[local]
Ltac mlTautoBreak := repeat match goal with
| [ |- @of_MLGoal ?Sgm (@mkMLGoal ?Sgm ?Ctx ?l ?g ?i) ]
⇒
lazymatch g with
| (⊥) ⇒
breakHyps l
| _ ⇒ mlApplyMeta (@useBasicReasoning _ _ _ i (@bot_elim _ _ g _))
end
end.
Ltac try_solve_pile2 fallthrough :=
lazymatch goal with
| [ |- ProofInfoLe _ _] ⇒ try apply pile_refl; try_solve_pile; fallthrough
| _ ⇒ idtac
end.
#[global]
Ltac mlTauto :=
_ensureProofMode;
unshelve(
try (
toNNF; (try_solve_pile2 shelve);
repeat mlIntro;
mlTautoBreak;
findContradiction_start
)
)
.
#[local]
Example conj_right {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( (b and (a or b) and !b and ( a or a) and a) ---> ⊥)
using AnyReasoning.
#[local]
Example condtradict_taut_2 {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i (a ---> ((! a) ---> b))
using AnyReasoning.
#[local]
Example taut {Σ : Signature} Γ a b c:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i ((a ---> b) ---> ((b ---> c) ---> ((a or b)---> c)))
using AnyReasoning.
#[local]
Example condtradict_taut_1 {Σ : Signature} Γ a:
well_formed a →
Γ ⊢i !(a and !a)
using AnyReasoning.
#[local]
Example notnot_taut_1 {Σ : Signature} Γ a:
well_formed a →
Γ ⊢i (! ! a ---> a)
using AnyReasoning.
#[local]
Lemma Peirce_taut {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ((((a ---> b) ---> a) ---> a))
using AnyReasoning.
fun (n : int) (a : constr) (phi : constr) : HeatResult ⇒
let found : (Pattern.context option) ref := { contents := None } in
for_nth_match n a phi
(fun ctx ⇒
found.(contents) := Some ctx; ()
);
match found.(contents) with
| None ⇒ throw_pm_exn (Message.concat (Message.of_string "heat: could not find match for pattern: '")
(Message.concat (Message.of_constr a)
(Message.concat (Message.of_string "' inside '")
(Message.concat (Message.of_constr phi)
(Message.concat (Message.of_string "' for occurrence ")
(Message.of_int n)
)
)
)
)
)
| Some ctx
⇒ (
let fr := constr:(fresh_evar $phi) in
let star_ident := Fresh.in_goal ident:(star) in
let star_eq := Fresh.in_goal ident:(star_eq) in
(*set (fr);*)
remember $fr as $star_ident eqn:star_eq;
let star_hyp := Control.hyp star_ident in
let ctxpat := Pattern.instantiate ctx constr:(patt_free_evar $star_hyp) in
let pc := constr:((@Build_PatternCtx _ $star_hyp $ctxpat)) in
let heq1 := Fresh.in_goal ident:(heq1) in
assert(heq1 : ($phi = (@emplace _ $pc $a)))
> [ abstract(
(* TODO: this is slow for bigger patterns *)
(ltac1:(star |- simplify_emplace_2 star) (Ltac1.of_ident star_ident);
reflexivity
))
| ()
];
{ star_ident := star_ident; star_eq := star_eq; pc := pc; ctx := ctx; ctx_pat := ctxpat; equality := heq1 }
)
end
.
Lemma cast_proof_ml_goal {Σ : Signature} Γ hyps goal goal' (e : goal = goal') (i : ProofInfo):
mkMLGoal Σ Γ hyps goal i →
mkMLGoal Σ Γ hyps goal' i .
Ltac2 mlRewrite (hiff : constr) (atn : int) :=
let thiff := Constr.type hiff in
(* we have to unfold derives otherwise this might not match *)
lazy_match! (eval unfold derives in $thiff) with
| _ ⊢i (?a <---> ?a') using _
⇒
unfold AnyReasoning;
lazy_match! goal with
| [ |- of_MLGoal (@mkMLGoal ?sgm ?g ?l ?p ( ?gpi))]
⇒
let hr : HeatResult := heat atn a p in
if ml_debug_rewrite then
Message.print (Message.concat (Message.of_string "Heating finished: ") (Message.of_constr (hr.(ctx_pat))))
else () ;
let heq := (* Control.hyp *) (hr.(equality)) in
let pc := (hr.(pc)) in
(* let var := (hr.(star_ident)) in
let ctx_p := (hr.(ctx_pat)) in *)
eapply (@cast_proof_ml_goal _ $g) with (goal := emplace $pc $a) >
[ ltac1:(heq |- rewrite [left in _ = left] heq; reflexivity) (Ltac1.of_ident heq) | ()];
Std.clear [hr.(equality)];
let wfC := Fresh.in_goal ident:(wfC) in
assert (wfC : PC_wf $pc = true) > [ ltac1:(unfold PC_wf; simpl; wf_auto2); Control.shelve () | ()] ;
let wfCpf := Control.hyp wfC in
Control.plus (fun () ⇒
apply (@MLGoal_rewriteIff $sgm $g _ _ $pc $l $gpi $wfCpf $hiff) >
[
(lazy_match! goal with
| [ |- of_MLGoal (@mkMLGoal ?_sgm ?g ?_l ?p _)]
⇒
let heq2 := Fresh.in_goal ident:(heq2) in
let plugged := Pattern.instantiate (hr.(ctx)) a' in
assert(heq2: ($p = $plugged))
> [
(* TODO: this is slow for bigger patterns *)
abstract (ltac1:(star |- simplify_emplace_2 star) (Ltac1.of_ident (hr.(star_ident)));
reflexivity
)
| ()
];
let heq2_pf := Control.hyp heq2 in
eapply (@cast_proof_ml_goal _ $g) >
[ rewrite $heq2_pf; reflexivity | ()];
Std.clear [wfC; heq2 ; (hr.(star_ident)); (hr.(star_eq))]
end)
| (ltac1:(star |- try_solve_complex_pile star) (Ltac1.of_ident (hr.(star_ident))))
]
)
(fun _ ⇒ throw_pm_exn (Message.concat (Message.of_string "mlRewrite: failed when rewriting '")
(Message.concat (Message.of_constr (a))
(Message.concat (Message.of_string "' to/from '")
(Message.concat (Message.of_constr (a'))
(Message.concat (Message.of_string "' in context ")
(Message.of_constr (pc))
)
)
)
)
)
)
| [ |- _] ⇒ throw_pm_exn_with_goal "mlRewrite: not in proof mode "
end
| ?x ⇒ throw_pm_exn (Message.concat (Message.of_string "mlRewrite: Given hypothesis is not an equivalence: ") (Message.of_constr x))
end.
Ltac2 rec constr_to_int (x : constr) : int :=
match! x with
| 0 ⇒ 0
| (S ?x') ⇒ Int.add 1 (constr_to_int x')
end.
Tactic Notation "mlRewrite" constr(Hiff) "at" constr(atn) :=
_ensureProofMode;
(let ff := ltac2:(hiff atn |-
mlRewrite
(Option.get (Ltac1.to_constr(hiff)))
(constr_to_int (Option.get (Ltac1.to_constr(atn))))
) in
ff Hiff atn);
fold AnyReasoning.
Lemma pf_iff_equiv_sym_meta {Σ : Signature} Γ A B i :
Γ ⊢i (A <---> B) using i →
Γ ⊢i (B <---> A) using i.
Tactic Notation "mlRewrite" "->" constr(Hiff) "at" constr(atn) :=
mlRewrite Hiff at atn.
Tactic Notation "mlRewrite" "<-" constr(Hiff) "at" constr(atn) :=
mlRewrite (@pf_iff_equiv_sym_meta _ _ _ _ _ Hiff) at atn.
Local Example ex_prf_rewrite_equiv_1 {Σ : Signature} Γ a a':
well_formed a →
well_formed a' →
Γ ⊢ a <---> a' →
Γ ⊢ a' →
Γ ⊢ a.
Local Example ex_prf_rewrite_equiv_foldl {Σ : Signature} Γ a a' l:
well_formed a →
well_formed a' →
Pattern.wf l →
Γ ⊢ a <---> a' →
Γ ⊢ foldr patt_imp a' l →
Γ ⊢ foldr patt_imp a l.
Local Example ex_prf_rewrite_equiv_2 {Σ : Signature} Γ a a' b x y z:
well_formed a →
well_formed a' →
well_formed (ex, b) →
Γ ⊢ a <---> a' →
Γ ⊢i (ex, ((patt_free_evar y) ---> (patt_free_evar z) ---> a ⋅ a ⋅ b ⋅ a ---> (patt_free_evar x)))
<---> (ex, ((patt_free_evar y) ---> (patt_free_evar z) ---> a ⋅ a' ⋅ b ⋅ a' ---> (patt_free_evar x)))
using AnyReasoning.
(* TODO: de-duplicate the code *)
Ltac2 rec convertToNNF_rewrite_pat := fun (ctx : constr) (p : constr) (i : constr) : unit ⇒
lazy_match! p with
| (! ! ?x) ⇒ (
let h' := Fresh.in_goal ident:(H) in
assert ($h' := (@not_not_eq _ $ctx $x ltac2:(wf_auto2 ())));
apply (@useBasicReasoning _ _ _ $i) in $h';
let h_constr := Control.hyp h' in
repeat (mlRewrite h_constr 1);
try (clear h');
convertToNNF_rewrite_pat ctx x i
)
| patt_not (patt_and ?x ?y) ⇒ (
let h' := Fresh.in_goal ident:(H) in
assert ($h' := (@deMorgan_nand _ $ctx $x $y ltac:(wf_auto2) ltac:(wf_auto2)));
apply (@useBasicReasoning _ _ _ $i) in $h';
let h_constr := Control.hyp h' in
repeat (mlRewrite h_constr 1);
try (clear h');
convertToNNF_rewrite_pat ctx constr:(!$x or !$y) i
)
| patt_not (patt_or ?x ?y) ⇒ (
let h' := Fresh.in_goal ident:(H) in
assert ($h' := (@deMorgan_nor _ $ctx $x $y ltac:(wf_auto2) ltac:(wf_auto2)));
apply (@useBasicReasoning _ _ _ $i) in $h';
let h_constr := Control.hyp h' in
repeat (mlRewrite h_constr 1);
try (clear h');
convertToNNF_rewrite_pat ctx constr:(!$x and !$y) i
)
| patt_not (?x ---> ?y) ⇒ (
let h' := Fresh.in_goal ident:(H) in
assert ($h' := (@nimpl_eq_and _ $ctx $x $y ltac:(wf_auto2) ltac:(wf_auto2)));
apply (@useBasicReasoning _ _ _ $i) in $h';
let h_constr := Control.hyp h' in
repeat (mlRewrite h_constr 1);
try (clear h');
convertToNNF_rewrite_pat ctx constr:($x and !$y) i
)
| (?x ---> ?y) ⇒ (
let h' := Fresh.in_goal ident:(H) in
assert ($h' := (@impl_eq_or _ $ctx $x $y ltac:(wf_auto2) ltac:(wf_auto2)));
apply (@useBasicReasoning _ _ _ $i) in $h';
let h_constr := Control.hyp h' in
repeat (mlRewrite h_constr 1);
try (clear h');
convertToNNF_rewrite_pat ctx constr:(!$x or $y) i
)
| patt_and ?x ?y ⇒ convertToNNF_rewrite_pat ctx x i; convertToNNF_rewrite_pat ctx y i
| patt_or ?x ?y ⇒ convertToNNF_rewrite_pat ctx x i; convertToNNF_rewrite_pat ctx y i
| _ ⇒ ()
end
.
Ltac2 toNNF () :=
repeat (do_mlRevertLast ());
lazy_match! goal with
| [ |- @of_MLGoal ?sgm (@mkMLGoal ?sgm ?ctx ?_ll ?g ?i) ]
⇒
do_mlApplyMetaRaw constr:(@useBasicReasoning _ _ _ $i (@not_not_elim $sgm $ctx $g ltac2:(wf_auto2 ())));
convertToNNF_rewrite_pat ctx constr:(!$g) i
end
.
Ltac toNNF := ltac2:(toNNF ()).
#[local] Example test_toNNF {Σ : Signature} Γ a b :
well_formed a →
well_formed b →
Γ ⊢i ( (b and (a or b) and !b and ( a or a) and a) ---> ⊥)
using BasicReasoning.
#[local]
Ltac rfindContradictionTo a ll k :=
match ll with
| ((mkNH _ ?name (! a)) :: ?m) ⇒
mlApply name; mlExactn k
| ((mkNH _ _ _) :: ?m) ⇒
rfindContradictionTo a m k
| _ ⇒ fail
end.
#[local]
Ltac findContradiction l k:=
match l with
| ((mkNH _ _ ?a) :: ?m) ⇒
match goal with
| [ |- @of_MLGoal ?Sgm (@mkMLGoal ?Sgm ?Ctx ?ll ?g ?i) ]
⇒
try rfindContradictionTo a ll k;
let kk := eval compute in ( k + 1 ) in
(findContradiction m kk)
end
| _ ⇒ fail
end.
#[local]
Ltac findContradiction_start :=
match goal with
| [ |- @of_MLGoal ?Sgm (@mkMLGoal ?Sgm ?Ctx ?l ?g ?i) ]
⇒
match goal with
| [ |- @of_MLGoal ?Sgm (@mkMLGoal ?Sgm ?Ctx ?l ?g ?i) ]
⇒
findContradiction l 0
end
end.
#[local]
Ltac breakHyps l :=
match l with
| ((mkNH _ ?name (?x and ?y)) :: ?m) ⇒
mlDestructAnd name
| ((mkNH _ ?name (?x or ?y)) :: ?m) ⇒
mlDestructOr name
| ((mkNH _ ?name ?x) :: ?m) ⇒
breakHyps m
end.
#[local]
Ltac mlTautoBreak := repeat match goal with
| [ |- @of_MLGoal ?Sgm (@mkMLGoal ?Sgm ?Ctx ?l ?g ?i) ]
⇒
lazymatch g with
| (⊥) ⇒
breakHyps l
| _ ⇒ mlApplyMeta (@useBasicReasoning _ _ _ i (@bot_elim _ _ g _))
end
end.
Ltac try_solve_pile2 fallthrough :=
lazymatch goal with
| [ |- ProofInfoLe _ _] ⇒ try apply pile_refl; try_solve_pile; fallthrough
| _ ⇒ idtac
end.
#[global]
Ltac mlTauto :=
_ensureProofMode;
unshelve(
try (
toNNF; (try_solve_pile2 shelve);
repeat mlIntro;
mlTautoBreak;
findContradiction_start
)
)
.
#[local]
Example conj_right {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ( (b and (a or b) and !b and ( a or a) and a) ---> ⊥)
using AnyReasoning.
#[local]
Example condtradict_taut_2 {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i (a ---> ((! a) ---> b))
using AnyReasoning.
#[local]
Example taut {Σ : Signature} Γ a b c:
well_formed a →
well_formed b →
well_formed c →
Γ ⊢i ((a ---> b) ---> ((b ---> c) ---> ((a or b)---> c)))
using AnyReasoning.
#[local]
Example condtradict_taut_1 {Σ : Signature} Γ a:
well_formed a →
Γ ⊢i !(a and !a)
using AnyReasoning.
#[local]
Example notnot_taut_1 {Σ : Signature} Γ a:
well_formed a →
Γ ⊢i (! ! a ---> a)
using AnyReasoning.
#[local]
Lemma Peirce_taut {Σ : Signature} Γ a b:
well_formed a →
well_formed b →
Γ ⊢i ((((a ---> b) ---> a) ---> a))
using AnyReasoning.
This page has been generated by coqdoc