File ProofInfo
From Ltac2 Require Export Ltac2.
From MatchingLogic Require Export ProofSystem
NamedAxioms.
Import
MatchingLogic.Syntax.Notations
MatchingLogic.DerivedOperators_Syntax.Notations
MatchingLogic.ProofSystem.Notations_private
.
Open Scope ml_scope.
Section with_signature.
Context {Σ : Signature}.
(* TODO make this return well-formed patterns. *)
Fixpoint framing_patterns Γ ϕ (pf : Γ ⊢H ϕ) : gset wfPattern :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ ∅
| ML_P1 _ _ _ _ _ ⇒ ∅
| ML_P2 _ _ _ _ _ _ _ ⇒ ∅
| ML_P3 _ _ _ ⇒ ∅
| ML_Modus_ponens _ _ _ m0 m1
⇒ (@framing_patterns _ _ m0) ∪ (@framing_patterns _ _ m1)
| ML_Ex_quan _ _ _ _ ⇒ ∅
| ML_Ex_gen _ _ _ x _ _ pf _ ⇒ @framing_patterns _ _ pf
| ML_Prop_bott_left _ _ _ ⇒ ∅
| ML_Prop_bott_right _ _ _ ⇒ ∅
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_left _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_right _ _ _ _ _ ⇒ ∅
| ML_Framing_left _ _ _ psi wfp m0 ⇒ {[(exist _ psi wfp)]} ∪ (@framing_patterns _ _ m0)
| ML_Framing_right _ _ _ psi wfp m0 ⇒ {[(exist _ psi wfp)]} ∪ (@framing_patterns _ _ m0)
| ML_Svar_subst _ _ _ _ _ _ m0 ⇒ @framing_patterns _ _ m0
| ML_Pre_fixp _ _ _ ⇒ ∅
| ML_Knaster_tarski _ _ phi psi m0 ⇒ @framing_patterns _ _ m0
| ML_Existence _ ⇒ ∅
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ ∅
end.
Fixpoint uses_ex_gen (EvS : EVarSet) Γ ϕ (pf : ML_proof_system Γ ϕ) :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ false
| ML_P1 _ _ _ _ _ ⇒ false
| ML_P2 _ _ _ _ _ _ _ ⇒ false
| ML_P3 _ _ _ ⇒ false
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_ex_gen EvS _ _ m0
|| uses_ex_gen EvS _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ false
| ML_Ex_gen _ _ _ x _ _ pf _ ⇒ if decide (x ∈ EvS) is left _ then true else uses_ex_gen EvS _ _ pf
| ML_Prop_bott_left _ _ _ ⇒ false
| ML_Prop_bott_right _ _ _ ⇒ false
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ false
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ false
| ML_Prop_ex_left _ _ _ _ _ ⇒ false
| ML_Prop_ex_right _ _ _ _ _ ⇒ false
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_ex_gen EvS _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_ex_gen EvS _ _ m0
| ML_Svar_subst _ _ _ _ _ _ m0 ⇒ uses_ex_gen EvS _ _ m0
| ML_Pre_fixp _ _ _ ⇒ false
| ML_Knaster_tarski _ _ phi psi m0 ⇒ uses_ex_gen EvS _ _ m0
| ML_Existence _ ⇒ false
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ false
end.
Fixpoint uses_of_ex_gen Γ ϕ (pf : ML_proof_system Γ ϕ) : EVarSet :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ ∅
| ML_P1 _ _ _ _ _ ⇒ ∅
| ML_P2 _ _ _ _ _ _ _ ⇒ ∅
| ML_P3 _ _ _ ⇒ ∅
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_of_ex_gen _ _ m0
∪ uses_of_ex_gen _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ ∅
| ML_Ex_gen _ _ _ x _ _ pf _ ⇒ {[x]} ∪ uses_of_ex_gen _ _ pf
| ML_Prop_bott_left _ _ _ ⇒ ∅
| ML_Prop_bott_right _ _ _ ⇒ ∅
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_left _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_right _ _ _ _ _ ⇒ ∅
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_of_ex_gen _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_of_ex_gen _ _ m0
| ML_Svar_subst _ _ _ _ _ _ m0 ⇒ uses_of_ex_gen _ _ m0
| ML_Pre_fixp _ _ _ ⇒ ∅
| ML_Knaster_tarski _ _ phi psi m0 ⇒ uses_of_ex_gen _ _ m0
| ML_Existence _ ⇒ ∅
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ ∅
end.
Lemma uses_of_ex_gen_correct Γ ϕ (pf : ML_proof_system Γ ϕ) (x : evar) :
x ∈ uses_of_ex_gen Γ ϕ pf ↔ uses_ex_gen {[x]} Γ ϕ pf = true.
Fixpoint uses_svar_subst (S : SVarSet) Γ ϕ (pf : Γ ⊢H ϕ) :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ false
| ML_P1 _ _ _ _ _ ⇒ false
| ML_P2 _ _ _ _ _ _ _ ⇒ false
| ML_P3 _ _ _ ⇒ false
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_svar_subst S _ _ m0
|| uses_svar_subst S _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ false
| ML_Ex_gen _ _ _ _ _ _ pf' _ ⇒ uses_svar_subst S _ _ pf'
| ML_Prop_bott_left _ _ _ ⇒ false
| ML_Prop_bott_right _ _ _ ⇒ false
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ false
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ false
| ML_Prop_ex_left _ _ _ _ _ ⇒ false
| ML_Prop_ex_right _ _ _ _ _ ⇒ false
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_svar_subst S _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_svar_subst S _ _ m0
| ML_Svar_subst _ _ _ X _ _ m0 ⇒ if decide (X ∈ S) is left _ then true else uses_svar_subst S _ _ m0
| ML_Pre_fixp _ _ _ ⇒ false
| ML_Knaster_tarski _ _ phi psi m0 ⇒ uses_svar_subst S _ _ m0
| ML_Existence _ ⇒ false
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ false
end.
Fixpoint uses_of_svar_subst Γ ϕ (pf : Γ ⊢H ϕ) : SVarSet :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ ∅
| ML_P1 _ _ _ _ _ ⇒ ∅
| ML_P2 _ _ _ _ _ _ _ ⇒ ∅
| ML_P3 _ _ _ ⇒ ∅
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_of_svar_subst _ _ m0
∪ uses_of_svar_subst _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ ∅
| ML_Ex_gen _ _ _ _ _ _ pf' _ ⇒ uses_of_svar_subst _ _ pf'
| ML_Prop_bott_left _ _ _ ⇒ ∅
| ML_Prop_bott_right _ _ _ ⇒ ∅
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_left _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_right _ _ _ _ _ ⇒ ∅
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_of_svar_subst _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_of_svar_subst _ _ m0
| ML_Svar_subst _ _ _ X _ _ m0 ⇒ {[X]} ∪ uses_of_svar_subst _ _ m0
| ML_Pre_fixp _ _ _ ⇒ ∅
| ML_Knaster_tarski _ _ phi psi m0 ⇒ uses_of_svar_subst _ _ m0
| ML_Existence _ ⇒ ∅
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ ∅
end.
Lemma uses_of_svar_subst_correct Γ ϕ (pf : ML_proof_system Γ ϕ) (X : svar) :
X ∈ uses_of_svar_subst Γ ϕ pf ↔ uses_svar_subst {[X]} Γ ϕ pf = true.
Fixpoint uses_kt Γ ϕ (pf : Γ ⊢H ϕ) :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ false
| ML_P1 _ _ _ _ _ ⇒ false
| ML_P2 _ _ _ _ _ _ _ ⇒ false
| ML_P3 _ _ _ ⇒ false
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_kt _ _ m0 || uses_kt _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ false
| ML_Ex_gen _ _ _ _ _ _ pf' _ ⇒ uses_kt _ _ pf'
| ML_Prop_bott_left _ _ _ ⇒ false
| ML_Prop_bott_right _ _ _ ⇒ false
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ false
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ false
| ML_Prop_ex_left _ _ _ _ _ ⇒ false
| ML_Prop_ex_right _ _ _ _ _ ⇒ false
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_kt _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_kt _ _ m0
| ML_Svar_subst _ _ _ X _ _ m0 ⇒ uses_kt _ _ m0
| ML_Pre_fixp _ _ _ ⇒ false
| ML_Knaster_tarski _ _ phi psi m0 ⇒ true
| ML_Existence _ ⇒ false
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ false
end.
Fixpoint propositional_only Γ ϕ (pf : Γ ⊢H ϕ) :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ true
| ML_P1 _ _ _ _ _ ⇒ true
| ML_P2 _ _ _ _ _ _ _ ⇒ true
| ML_P3 _ _ _ ⇒ true
| ML_Modus_ponens _ _ _ m0 m1
⇒ propositional_only _ _ m0 && propositional_only _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ false
| ML_Ex_gen _ _ _ _ _ _ pf' _ ⇒ false
| ML_Prop_bott_left _ _ _ ⇒ false
| ML_Prop_bott_right _ _ _ ⇒ false
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ false
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ false
| ML_Prop_ex_left _ _ _ _ _ ⇒ false
| ML_Prop_ex_right _ _ _ _ _ ⇒ false
| ML_Framing_left _ _ _ _ _ m0 ⇒ false
| ML_Framing_right _ _ _ _ _ m0 ⇒ false
| ML_Svar_subst _ _ _ X _ _ m0 ⇒ false
| ML_Pre_fixp _ _ _ ⇒ false
| ML_Knaster_tarski _ _ phi psi m0 ⇒ false
| ML_Existence _ ⇒ false
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ false
end.
Lemma propositional_implies_no_frame Γ ϕ (pf : Γ ⊢H ϕ) :
propositional_only Γ ϕ pf = true → framing_patterns Γ ϕ pf = ∅.
Lemma propositional_implies_noKT Γ ϕ (pf : Γ ⊢H ϕ) :
propositional_only Γ ϕ pf = true → uses_kt Γ ϕ pf = false.
Lemma propositional_implies_no_uses_svar Γ ϕ (pf : ML_proof_system Γ ϕ) (SvS : SVarSet) :
propositional_only Γ ϕ pf = true → uses_svar_subst SvS Γ ϕ pf = false.
Lemma propositional_implies_no_uses_ex_gen Γ ϕ (pf : ML_proof_system Γ ϕ) (EvS : EVarSet) :
propositional_only Γ ϕ pf = true → uses_ex_gen EvS Γ ϕ pf = false.
Lemma propositional_implies_no_uses_ex_gen_2 Γ ϕ (pf : ML_proof_system Γ ϕ) :
propositional_only Γ ϕ pf = true → uses_of_ex_gen Γ ϕ pf = ∅.
Lemma propositional_implies_no_uses_svar_2 Γ ϕ (pf : ML_proof_system Γ ϕ) :
propositional_only Γ ϕ pf = true → uses_of_svar_subst Γ ϕ pf = ∅.
Definition proofbpred := ∀ (Γ : Theory) (ϕ : Pattern), Γ ⊢H ϕ → bool.
Definition indifferent_to_cast (P : proofbpred)
:= ∀ (Γ : Theory) (ϕ ψ : Pattern) (e: ψ = ϕ) (pf : Γ ⊢H ϕ),
P Γ ψ (cast_proof e pf) = P Γ ϕ pf.
Lemma indifferent_to_cast_uses_svar_subst SvS:
indifferent_to_cast (uses_svar_subst SvS).
Lemma indifferent_to_cast_uses_kt:
indifferent_to_cast uses_kt.
Lemma indifferent_to_cast_uses_ex_gen EvS:
indifferent_to_cast (uses_ex_gen EvS).
End with_signature.
Definition has_bound_variable_under_mu {Σ : Signature} (ϕ : Pattern) : bool
:= let x := fresh_evar ϕ in
mu_in_evar_path x (bsvar_subst (patt_free_evar x) 0 ϕ) 0
.
Fixpoint uses_kt_unreasonably {Σ : Signature} Γ ϕ (pf : ML_proof_system Γ ϕ) :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ false
| ML_P1 _ _ _ _ _ ⇒ false
| ML_P2 _ _ _ _ _ _ _ ⇒ false
| ML_P3 _ _ _ ⇒ false
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_kt_unreasonably _ _ m0 || uses_kt_unreasonably _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ false
| ML_Ex_gen _ _ _ _ _ _ pf' _ ⇒ uses_kt_unreasonably _ _ pf'
| ML_Prop_bott_left _ _ _ ⇒ false
| ML_Prop_bott_right _ _ _ ⇒ false
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ false
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ false
| ML_Prop_ex_left _ _ _ _ _ ⇒ false
| ML_Prop_ex_right _ _ _ _ _ ⇒ false
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_kt_unreasonably _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_kt_unreasonably _ _ m0
| ML_Svar_subst _ _ _ X _ _ m0 ⇒ uses_kt_unreasonably _ _ m0
| ML_Pre_fixp _ _ _ ⇒ false
| ML_Knaster_tarski _ phi psi wf m0 ⇒
(*has_bound_variable_under_mu phi ||*)
~~ (bound_svar_is_banned_under_mus phi 0 0) ||
uses_kt_unreasonably _ _ m0
| ML_Existence _ ⇒ false
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ false
end.
Lemma indifferent_to_cast_uses_kt_unreasonably {Σ : Signature}:
indifferent_to_cast uses_kt_unreasonably.
Lemma kt_unreasonably_implies_somehow {Σ : Signature} Γ ϕ (pf : ML_proof_system Γ ϕ) :
uses_kt_unreasonably Γ ϕ pf → uses_kt Γ ϕ pf.
Arguments uses_svar_subst {Σ} S {Γ} {ϕ} pf : rename.
Arguments uses_kt {Σ} {Γ} {ϕ} pf : rename.
Arguments uses_kt_unreasonably {Σ} {Γ} {ϕ} pf : rename.
Arguments uses_ex_gen {Σ} E {Γ} {ϕ} pf : rename.
Section proof_constraint.
Context {Σ : Signature}.
Lemma instantiate_named_axiom (NA : NamedAxioms) (name : (NAName NA)) :
(theory_of_NamedAxioms NA) ⊢H (@NAAxiom Σ NA name).
Definition coEVarSet := coGset evar.
Definition coSVarSet := coGset svar.
Definition WfpSet := gmap.gset wfPattern.
Definition coWfpSet := coGset wfPattern.
Record ProofInfo :=
mkProofInfo
{
pi_generalized_evars : coEVarSet ;
pi_substituted_svars : coSVarSet ;
pi_uses_kt : bool ;
pi_uses_advanced_kt : bool ;
(* pi_framing_patterns : coWfpSet ; *)
}.
Definition ProofInfoLe (i₁ i₂ : ProofInfo) : Prop :=
pi_generalized_evars i₁ ⊆ pi_generalized_evars i₂ ∧
pi_substituted_svars i₁ ⊆ pi_substituted_svars i₂ ∧
(pi_uses_kt i₁ ==> pi_uses_kt i₂) ∧
(pi_uses_advanced_kt i₁ ==> pi_uses_advanced_kt i₂)
.
(* A proof together with some properties of it. *)
Record ProofInfoMeaning
(Γ : Theory)
(ϕ : Pattern)
(pwi_pf : Γ ⊢H ϕ)
(pi : ProofInfo)
: Prop
:=
mkProofInfoMeaning
{
pwi_pf_ge : gset_to_coGset (@uses_of_ex_gen Σ Γ ϕ pwi_pf) ⊆ pi_generalized_evars pi ;
pwi_pf_svs : gset_to_coGset (@uses_of_svar_subst Σ Γ ϕ pwi_pf) ⊆ pi_substituted_svars pi ;
pwi_pf_kt : implb (@uses_kt Σ Γ ϕ pwi_pf) (pi_uses_kt pi) ;
pwi_pf_kta : implb (@uses_kt_unreasonably Σ Γ ϕ pwi_pf) (pi_uses_advanced_kt pi && (@uses_kt Σ Γ ϕ pwi_pf)) ;
(* pwi_pf_fp : gset_to_coGset (@framing_patterns Σ Γ ϕ pwi_pf) ⊆ (pi_framing_patterns pi) ; *)
}.
Definition ProofLe (i₁ i₂ : ProofInfo) :=
∀ (Γ : Theory) (ϕ : Pattern) (pf : Γ ⊢H ϕ),
@ProofInfoMeaning Γ ϕ pf i₁ → @ProofInfoMeaning Γ ϕ pf i₂.
Lemma ProofInfoLe_ProofLe (i₁ i₂ : ProofInfo) :
ProofInfoLe i₁ i₂ → ProofLe i₁ i₂.
End proof_constraint.
Ltac convert_implb :=
unfold is_true in *;
match goal with
| |- context G [implb _ _ = true] ⇒ rewrite implb_true_iff
| H : context G [implb _ _ = true] |- _ ⇒ rewrite implb_true_iff in H
end.
Ltac convert_orb :=
unfold is_true in *;
match goal with
| |- context G [orb _ _ = true] ⇒ rewrite orb_true_iff
| H : context G [orb _ _ = true] |- _ ⇒ rewrite orb_true_iff in H
end.
Ltac convert_andb :=
unfold is_true in *;
match goal with
| |- context G [orb _ _ = true] ⇒ rewrite andb_true_iff
| H : context G [orb _ _ = true] |- _ ⇒ rewrite andb_true_iff in H
end.
Ltac destruct_pile :=
match goal with
| H : @ProofInfoLe _ _ _ |- _ ⇒ destruct H as [? [? ?] ]
end.
From MatchingLogic Require Export ProofSystem
NamedAxioms.
Import
MatchingLogic.Syntax.Notations
MatchingLogic.DerivedOperators_Syntax.Notations
MatchingLogic.ProofSystem.Notations_private
.
Open Scope ml_scope.
Section with_signature.
Context {Σ : Signature}.
(* TODO make this return well-formed patterns. *)
Fixpoint framing_patterns Γ ϕ (pf : Γ ⊢H ϕ) : gset wfPattern :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ ∅
| ML_P1 _ _ _ _ _ ⇒ ∅
| ML_P2 _ _ _ _ _ _ _ ⇒ ∅
| ML_P3 _ _ _ ⇒ ∅
| ML_Modus_ponens _ _ _ m0 m1
⇒ (@framing_patterns _ _ m0) ∪ (@framing_patterns _ _ m1)
| ML_Ex_quan _ _ _ _ ⇒ ∅
| ML_Ex_gen _ _ _ x _ _ pf _ ⇒ @framing_patterns _ _ pf
| ML_Prop_bott_left _ _ _ ⇒ ∅
| ML_Prop_bott_right _ _ _ ⇒ ∅
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_left _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_right _ _ _ _ _ ⇒ ∅
| ML_Framing_left _ _ _ psi wfp m0 ⇒ {[(exist _ psi wfp)]} ∪ (@framing_patterns _ _ m0)
| ML_Framing_right _ _ _ psi wfp m0 ⇒ {[(exist _ psi wfp)]} ∪ (@framing_patterns _ _ m0)
| ML_Svar_subst _ _ _ _ _ _ m0 ⇒ @framing_patterns _ _ m0
| ML_Pre_fixp _ _ _ ⇒ ∅
| ML_Knaster_tarski _ _ phi psi m0 ⇒ @framing_patterns _ _ m0
| ML_Existence _ ⇒ ∅
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ ∅
end.
Fixpoint uses_ex_gen (EvS : EVarSet) Γ ϕ (pf : ML_proof_system Γ ϕ) :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ false
| ML_P1 _ _ _ _ _ ⇒ false
| ML_P2 _ _ _ _ _ _ _ ⇒ false
| ML_P3 _ _ _ ⇒ false
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_ex_gen EvS _ _ m0
|| uses_ex_gen EvS _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ false
| ML_Ex_gen _ _ _ x _ _ pf _ ⇒ if decide (x ∈ EvS) is left _ then true else uses_ex_gen EvS _ _ pf
| ML_Prop_bott_left _ _ _ ⇒ false
| ML_Prop_bott_right _ _ _ ⇒ false
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ false
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ false
| ML_Prop_ex_left _ _ _ _ _ ⇒ false
| ML_Prop_ex_right _ _ _ _ _ ⇒ false
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_ex_gen EvS _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_ex_gen EvS _ _ m0
| ML_Svar_subst _ _ _ _ _ _ m0 ⇒ uses_ex_gen EvS _ _ m0
| ML_Pre_fixp _ _ _ ⇒ false
| ML_Knaster_tarski _ _ phi psi m0 ⇒ uses_ex_gen EvS _ _ m0
| ML_Existence _ ⇒ false
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ false
end.
Fixpoint uses_of_ex_gen Γ ϕ (pf : ML_proof_system Γ ϕ) : EVarSet :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ ∅
| ML_P1 _ _ _ _ _ ⇒ ∅
| ML_P2 _ _ _ _ _ _ _ ⇒ ∅
| ML_P3 _ _ _ ⇒ ∅
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_of_ex_gen _ _ m0
∪ uses_of_ex_gen _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ ∅
| ML_Ex_gen _ _ _ x _ _ pf _ ⇒ {[x]} ∪ uses_of_ex_gen _ _ pf
| ML_Prop_bott_left _ _ _ ⇒ ∅
| ML_Prop_bott_right _ _ _ ⇒ ∅
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_left _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_right _ _ _ _ _ ⇒ ∅
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_of_ex_gen _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_of_ex_gen _ _ m0
| ML_Svar_subst _ _ _ _ _ _ m0 ⇒ uses_of_ex_gen _ _ m0
| ML_Pre_fixp _ _ _ ⇒ ∅
| ML_Knaster_tarski _ _ phi psi m0 ⇒ uses_of_ex_gen _ _ m0
| ML_Existence _ ⇒ ∅
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ ∅
end.
Lemma uses_of_ex_gen_correct Γ ϕ (pf : ML_proof_system Γ ϕ) (x : evar) :
x ∈ uses_of_ex_gen Γ ϕ pf ↔ uses_ex_gen {[x]} Γ ϕ pf = true.
Fixpoint uses_svar_subst (S : SVarSet) Γ ϕ (pf : Γ ⊢H ϕ) :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ false
| ML_P1 _ _ _ _ _ ⇒ false
| ML_P2 _ _ _ _ _ _ _ ⇒ false
| ML_P3 _ _ _ ⇒ false
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_svar_subst S _ _ m0
|| uses_svar_subst S _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ false
| ML_Ex_gen _ _ _ _ _ _ pf' _ ⇒ uses_svar_subst S _ _ pf'
| ML_Prop_bott_left _ _ _ ⇒ false
| ML_Prop_bott_right _ _ _ ⇒ false
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ false
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ false
| ML_Prop_ex_left _ _ _ _ _ ⇒ false
| ML_Prop_ex_right _ _ _ _ _ ⇒ false
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_svar_subst S _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_svar_subst S _ _ m0
| ML_Svar_subst _ _ _ X _ _ m0 ⇒ if decide (X ∈ S) is left _ then true else uses_svar_subst S _ _ m0
| ML_Pre_fixp _ _ _ ⇒ false
| ML_Knaster_tarski _ _ phi psi m0 ⇒ uses_svar_subst S _ _ m0
| ML_Existence _ ⇒ false
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ false
end.
Fixpoint uses_of_svar_subst Γ ϕ (pf : Γ ⊢H ϕ) : SVarSet :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ ∅
| ML_P1 _ _ _ _ _ ⇒ ∅
| ML_P2 _ _ _ _ _ _ _ ⇒ ∅
| ML_P3 _ _ _ ⇒ ∅
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_of_svar_subst _ _ m0
∪ uses_of_svar_subst _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ ∅
| ML_Ex_gen _ _ _ _ _ _ pf' _ ⇒ uses_of_svar_subst _ _ pf'
| ML_Prop_bott_left _ _ _ ⇒ ∅
| ML_Prop_bott_right _ _ _ ⇒ ∅
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_left _ _ _ _ _ ⇒ ∅
| ML_Prop_ex_right _ _ _ _ _ ⇒ ∅
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_of_svar_subst _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_of_svar_subst _ _ m0
| ML_Svar_subst _ _ _ X _ _ m0 ⇒ {[X]} ∪ uses_of_svar_subst _ _ m0
| ML_Pre_fixp _ _ _ ⇒ ∅
| ML_Knaster_tarski _ _ phi psi m0 ⇒ uses_of_svar_subst _ _ m0
| ML_Existence _ ⇒ ∅
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ ∅
end.
Lemma uses_of_svar_subst_correct Γ ϕ (pf : ML_proof_system Γ ϕ) (X : svar) :
X ∈ uses_of_svar_subst Γ ϕ pf ↔ uses_svar_subst {[X]} Γ ϕ pf = true.
Fixpoint uses_kt Γ ϕ (pf : Γ ⊢H ϕ) :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ false
| ML_P1 _ _ _ _ _ ⇒ false
| ML_P2 _ _ _ _ _ _ _ ⇒ false
| ML_P3 _ _ _ ⇒ false
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_kt _ _ m0 || uses_kt _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ false
| ML_Ex_gen _ _ _ _ _ _ pf' _ ⇒ uses_kt _ _ pf'
| ML_Prop_bott_left _ _ _ ⇒ false
| ML_Prop_bott_right _ _ _ ⇒ false
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ false
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ false
| ML_Prop_ex_left _ _ _ _ _ ⇒ false
| ML_Prop_ex_right _ _ _ _ _ ⇒ false
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_kt _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_kt _ _ m0
| ML_Svar_subst _ _ _ X _ _ m0 ⇒ uses_kt _ _ m0
| ML_Pre_fixp _ _ _ ⇒ false
| ML_Knaster_tarski _ _ phi psi m0 ⇒ true
| ML_Existence _ ⇒ false
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ false
end.
Fixpoint propositional_only Γ ϕ (pf : Γ ⊢H ϕ) :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ true
| ML_P1 _ _ _ _ _ ⇒ true
| ML_P2 _ _ _ _ _ _ _ ⇒ true
| ML_P3 _ _ _ ⇒ true
| ML_Modus_ponens _ _ _ m0 m1
⇒ propositional_only _ _ m0 && propositional_only _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ false
| ML_Ex_gen _ _ _ _ _ _ pf' _ ⇒ false
| ML_Prop_bott_left _ _ _ ⇒ false
| ML_Prop_bott_right _ _ _ ⇒ false
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ false
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ false
| ML_Prop_ex_left _ _ _ _ _ ⇒ false
| ML_Prop_ex_right _ _ _ _ _ ⇒ false
| ML_Framing_left _ _ _ _ _ m0 ⇒ false
| ML_Framing_right _ _ _ _ _ m0 ⇒ false
| ML_Svar_subst _ _ _ X _ _ m0 ⇒ false
| ML_Pre_fixp _ _ _ ⇒ false
| ML_Knaster_tarski _ _ phi psi m0 ⇒ false
| ML_Existence _ ⇒ false
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ false
end.
Lemma propositional_implies_no_frame Γ ϕ (pf : Γ ⊢H ϕ) :
propositional_only Γ ϕ pf = true → framing_patterns Γ ϕ pf = ∅.
Lemma propositional_implies_noKT Γ ϕ (pf : Γ ⊢H ϕ) :
propositional_only Γ ϕ pf = true → uses_kt Γ ϕ pf = false.
Lemma propositional_implies_no_uses_svar Γ ϕ (pf : ML_proof_system Γ ϕ) (SvS : SVarSet) :
propositional_only Γ ϕ pf = true → uses_svar_subst SvS Γ ϕ pf = false.
Lemma propositional_implies_no_uses_ex_gen Γ ϕ (pf : ML_proof_system Γ ϕ) (EvS : EVarSet) :
propositional_only Γ ϕ pf = true → uses_ex_gen EvS Γ ϕ pf = false.
Lemma propositional_implies_no_uses_ex_gen_2 Γ ϕ (pf : ML_proof_system Γ ϕ) :
propositional_only Γ ϕ pf = true → uses_of_ex_gen Γ ϕ pf = ∅.
Lemma propositional_implies_no_uses_svar_2 Γ ϕ (pf : ML_proof_system Γ ϕ) :
propositional_only Γ ϕ pf = true → uses_of_svar_subst Γ ϕ pf = ∅.
Definition proofbpred := ∀ (Γ : Theory) (ϕ : Pattern), Γ ⊢H ϕ → bool.
Definition indifferent_to_cast (P : proofbpred)
:= ∀ (Γ : Theory) (ϕ ψ : Pattern) (e: ψ = ϕ) (pf : Γ ⊢H ϕ),
P Γ ψ (cast_proof e pf) = P Γ ϕ pf.
Lemma indifferent_to_cast_uses_svar_subst SvS:
indifferent_to_cast (uses_svar_subst SvS).
Lemma indifferent_to_cast_uses_kt:
indifferent_to_cast uses_kt.
Lemma indifferent_to_cast_uses_ex_gen EvS:
indifferent_to_cast (uses_ex_gen EvS).
End with_signature.
Definition has_bound_variable_under_mu {Σ : Signature} (ϕ : Pattern) : bool
:= let x := fresh_evar ϕ in
mu_in_evar_path x (bsvar_subst (patt_free_evar x) 0 ϕ) 0
.
Fixpoint uses_kt_unreasonably {Σ : Signature} Γ ϕ (pf : ML_proof_system Γ ϕ) :=
match pf with
| ML_hypothesis _ _ _ _ ⇒ false
| ML_P1 _ _ _ _ _ ⇒ false
| ML_P2 _ _ _ _ _ _ _ ⇒ false
| ML_P3 _ _ _ ⇒ false
| ML_Modus_ponens _ _ _ m0 m1
⇒ uses_kt_unreasonably _ _ m0 || uses_kt_unreasonably _ _ m1
| ML_Ex_quan _ _ _ _ ⇒ false
| ML_Ex_gen _ _ _ _ _ _ pf' _ ⇒ uses_kt_unreasonably _ _ pf'
| ML_Prop_bott_left _ _ _ ⇒ false
| ML_Prop_bott_right _ _ _ ⇒ false
| ML_Prop_disj_left _ _ _ _ _ _ _ ⇒ false
| ML_Prop_disj_right _ _ _ _ _ _ _ ⇒ false
| ML_Prop_ex_left _ _ _ _ _ ⇒ false
| ML_Prop_ex_right _ _ _ _ _ ⇒ false
| ML_Framing_left _ _ _ _ _ m0 ⇒ uses_kt_unreasonably _ _ m0
| ML_Framing_right _ _ _ _ _ m0 ⇒ uses_kt_unreasonably _ _ m0
| ML_Svar_subst _ _ _ X _ _ m0 ⇒ uses_kt_unreasonably _ _ m0
| ML_Pre_fixp _ _ _ ⇒ false
| ML_Knaster_tarski _ phi psi wf m0 ⇒
(*has_bound_variable_under_mu phi ||*)
~~ (bound_svar_is_banned_under_mus phi 0 0) ||
uses_kt_unreasonably _ _ m0
| ML_Existence _ ⇒ false
| ML_Singleton_ctx _ _ _ _ _ _ ⇒ false
end.
Lemma indifferent_to_cast_uses_kt_unreasonably {Σ : Signature}:
indifferent_to_cast uses_kt_unreasonably.
Lemma kt_unreasonably_implies_somehow {Σ : Signature} Γ ϕ (pf : ML_proof_system Γ ϕ) :
uses_kt_unreasonably Γ ϕ pf → uses_kt Γ ϕ pf.
Arguments uses_svar_subst {Σ} S {Γ} {ϕ} pf : rename.
Arguments uses_kt {Σ} {Γ} {ϕ} pf : rename.
Arguments uses_kt_unreasonably {Σ} {Γ} {ϕ} pf : rename.
Arguments uses_ex_gen {Σ} E {Γ} {ϕ} pf : rename.
Section proof_constraint.
Context {Σ : Signature}.
Lemma instantiate_named_axiom (NA : NamedAxioms) (name : (NAName NA)) :
(theory_of_NamedAxioms NA) ⊢H (@NAAxiom Σ NA name).
Definition coEVarSet := coGset evar.
Definition coSVarSet := coGset svar.
Definition WfpSet := gmap.gset wfPattern.
Definition coWfpSet := coGset wfPattern.
Record ProofInfo :=
mkProofInfo
{
pi_generalized_evars : coEVarSet ;
pi_substituted_svars : coSVarSet ;
pi_uses_kt : bool ;
pi_uses_advanced_kt : bool ;
(* pi_framing_patterns : coWfpSet ; *)
}.
Definition ProofInfoLe (i₁ i₂ : ProofInfo) : Prop :=
pi_generalized_evars i₁ ⊆ pi_generalized_evars i₂ ∧
pi_substituted_svars i₁ ⊆ pi_substituted_svars i₂ ∧
(pi_uses_kt i₁ ==> pi_uses_kt i₂) ∧
(pi_uses_advanced_kt i₁ ==> pi_uses_advanced_kt i₂)
.
(* A proof together with some properties of it. *)
Record ProofInfoMeaning
(Γ : Theory)
(ϕ : Pattern)
(pwi_pf : Γ ⊢H ϕ)
(pi : ProofInfo)
: Prop
:=
mkProofInfoMeaning
{
pwi_pf_ge : gset_to_coGset (@uses_of_ex_gen Σ Γ ϕ pwi_pf) ⊆ pi_generalized_evars pi ;
pwi_pf_svs : gset_to_coGset (@uses_of_svar_subst Σ Γ ϕ pwi_pf) ⊆ pi_substituted_svars pi ;
pwi_pf_kt : implb (@uses_kt Σ Γ ϕ pwi_pf) (pi_uses_kt pi) ;
pwi_pf_kta : implb (@uses_kt_unreasonably Σ Γ ϕ pwi_pf) (pi_uses_advanced_kt pi && (@uses_kt Σ Γ ϕ pwi_pf)) ;
(* pwi_pf_fp : gset_to_coGset (@framing_patterns Σ Γ ϕ pwi_pf) ⊆ (pi_framing_patterns pi) ; *)
}.
Definition ProofLe (i₁ i₂ : ProofInfo) :=
∀ (Γ : Theory) (ϕ : Pattern) (pf : Γ ⊢H ϕ),
@ProofInfoMeaning Γ ϕ pf i₁ → @ProofInfoMeaning Γ ϕ pf i₂.
Lemma ProofInfoLe_ProofLe (i₁ i₂ : ProofInfo) :
ProofInfoLe i₁ i₂ → ProofLe i₁ i₂.
End proof_constraint.
Ltac convert_implb :=
unfold is_true in *;
match goal with
| |- context G [implb _ _ = true] ⇒ rewrite implb_true_iff
| H : context G [implb _ _ = true] |- _ ⇒ rewrite implb_true_iff in H
end.
Ltac convert_orb :=
unfold is_true in *;
match goal with
| |- context G [orb _ _ = true] ⇒ rewrite orb_true_iff
| H : context G [orb _ _ = true] |- _ ⇒ rewrite orb_true_iff in H
end.
Ltac convert_andb :=
unfold is_true in *;
match goal with
| |- context G [orb _ _ = true] ⇒ rewrite andb_true_iff
| H : context G [orb _ _ = true] |- _ ⇒ rewrite andb_true_iff in H
end.
Ltac destruct_pile :=
match goal with
| H : @ProofInfoLe _ _ _ |- _ ⇒ destruct H as [? [? ?] ]
end.
To solve goals shaped like: ProofInfoLe i₁ i₂
Ltac try_solve_pile :=
assumption + (* optimization *)
(repeat destruct_pile;
simpl in *;
split; [try set_solver|split;[try set_solver
|try (repeat convert_implb;
repeat convert_orb;
repeat convert_andb;
set_solver)] ]).
Section proof_info.
Context {Σ : Signature}.
Import Notations_private.
(*
[global] Instance *)
Lemma pile_refl (i : ProofInfo) : ProofInfoLe i i.
(*
[global] Instance *)
Lemma pile_trans
(i₁ i₂ i₃ : ProofInfo) (PILE12 : ProofInfoLe i₁ i₂) (PILE23 : ProofInfoLe i₂ i₃)
: ProofInfoLe i₁ i₃.
Definition BasicReasoning : ProofInfo := ((@mkProofInfo _ ∅ ∅ false false)).
Definition AnyReasoning : ProofInfo := (@mkProofInfo _ ⊤ ⊤ true true).
Definition derives_using Γ ϕ pi
:= ({pf : Γ ⊢H ϕ | @ProofInfoMeaning _ _ _ pf pi }).
Definition derives Γ ϕ
:= derives_using Γ ϕ AnyReasoning.
Definition raw_proof_of {Γ} {ϕ} {pi}:
derives_using Γ ϕ pi →
ML_proof_system Γ ϕ
:= fun pf ⇒ proj1_sig pf.
End proof_info.
Module Notations.
Notation "Γ '⊢i' ϕ 'using' pi"
:= (derives_using Γ ϕ pi) (at level 95, no associativity).
Notation "Γ ⊢ ϕ" := (derives Γ ϕ)
(at level 95, no associativity).
Notation "'ExGen' ':=' evs ',' 'SVSubst' := svs ',' 'KT' := bkt ',' 'AKT' := akt"
:= (@mkProofInfo _ evs svs bkt akt) (at level 95, no associativity).
End Notations.
(* We cannot turn a proof into wellformedness hypotheses
if there is a ProofLe hypothesis depending on the proof
*)
Ltac2 clear_piles () :=
repeat (
lazy_match! goal with
| [ h : @ProofInfoLe _ _ _ |- _]
⇒ clear $h
| [ h : @ProofLe _ _ _ |- _]
⇒ clear $h
| [ h : @ProofInfoMeaning _ _ _ _ _ |- _]
⇒ clear $h
end
)
.
Ltac2 pfs_to_wfs () :=
repeat (
match! goal with
| [h : @derives _ _ _ |- _]
⇒ unfold derives in $h; unfold derives
| [h : @derives_using _ _ _ _ |- _]
⇒ apply @raw_proof_of in $h
| [ h: @ML_proof_system _ _ _ |- _]
⇒ apply @proved_impl_wf in $h
end
).
Ltac2 Set proved_hook_wfauto as oldhook
:= (fun () ⇒ (*Message.print (Message.of_string "hook_wfauto p2w");*) clear_piles (); pfs_to_wfs () (*; oldhook ()*)).
(*
Ltac2 Set hook_wfauto
:= (fun () => Message.print (Message.of_string "hook_wfauto p2w")).
*)
assumption + (* optimization *)
(repeat destruct_pile;
simpl in *;
split; [try set_solver|split;[try set_solver
|try (repeat convert_implb;
repeat convert_orb;
repeat convert_andb;
set_solver)] ]).
Section proof_info.
Context {Σ : Signature}.
Import Notations_private.
(*
[global] Instance *)
Lemma pile_refl (i : ProofInfo) : ProofInfoLe i i.
(*
[global] Instance *)
Lemma pile_trans
(i₁ i₂ i₃ : ProofInfo) (PILE12 : ProofInfoLe i₁ i₂) (PILE23 : ProofInfoLe i₂ i₃)
: ProofInfoLe i₁ i₃.
Definition BasicReasoning : ProofInfo := ((@mkProofInfo _ ∅ ∅ false false)).
Definition AnyReasoning : ProofInfo := (@mkProofInfo _ ⊤ ⊤ true true).
Definition derives_using Γ ϕ pi
:= ({pf : Γ ⊢H ϕ | @ProofInfoMeaning _ _ _ pf pi }).
Definition derives Γ ϕ
:= derives_using Γ ϕ AnyReasoning.
Definition raw_proof_of {Γ} {ϕ} {pi}:
derives_using Γ ϕ pi →
ML_proof_system Γ ϕ
:= fun pf ⇒ proj1_sig pf.
End proof_info.
Module Notations.
Notation "Γ '⊢i' ϕ 'using' pi"
:= (derives_using Γ ϕ pi) (at level 95, no associativity).
Notation "Γ ⊢ ϕ" := (derives Γ ϕ)
(at level 95, no associativity).
Notation "'ExGen' ':=' evs ',' 'SVSubst' := svs ',' 'KT' := bkt ',' 'AKT' := akt"
:= (@mkProofInfo _ evs svs bkt akt) (at level 95, no associativity).
End Notations.
(* We cannot turn a proof into wellformedness hypotheses
if there is a ProofLe hypothesis depending on the proof
*)
Ltac2 clear_piles () :=
repeat (
lazy_match! goal with
| [ h : @ProofInfoLe _ _ _ |- _]
⇒ clear $h
| [ h : @ProofLe _ _ _ |- _]
⇒ clear $h
| [ h : @ProofInfoMeaning _ _ _ _ _ |- _]
⇒ clear $h
end
)
.
Ltac2 pfs_to_wfs () :=
repeat (
match! goal with
| [h : @derives _ _ _ |- _]
⇒ unfold derives in $h; unfold derives
| [h : @derives_using _ _ _ _ |- _]
⇒ apply @raw_proof_of in $h
| [ h: @ML_proof_system _ _ _ |- _]
⇒ apply @proved_impl_wf in $h
end
).
Ltac2 Set proved_hook_wfauto as oldhook
:= (fun () ⇒ (*Message.print (Message.of_string "hook_wfauto p2w");*) clear_piles (); pfs_to_wfs () (*; oldhook ()*)).
(*
Ltac2 Set hook_wfauto
:= (fun () => Message.print (Message.of_string "hook_wfauto p2w")).
*)
For goals shaped like ProoInforMeeaning _ BasicReasoning
Ltac solve_pim_simple := constructor; simpl;[(set_solver)|(set_solver)|(reflexivity)|(reflexivity)].
Import Notations.
Lemma useBasicReasoning {Σ : Signature} {Γ : Theory} {ϕ : Pattern} (i : ProofInfo) :
Γ ⊢i ϕ using BasicReasoning →
Γ ⊢i ϕ using i.
Tactic Notation "remember_constraint" "as" ident(i') :=
match goal with
| [|- (_ ⊢i _ using ?constraint)] ⇒ remember constraint as i'
end.
Lemma useGenericReasoning {Σ : Signature} (Γ : Theory) (ϕ : Pattern) i' i:
(ProofInfoLe i' i) →
Γ ⊢i ϕ using i' →
Γ ⊢i ϕ using i.
Tactic Notation "gapply" uconstr(pf) := eapply useGenericReasoning;[|eapply pf].
Tactic Notation "gapply" uconstr(pf) "in" ident(H) :=
eapply useGenericReasoning in H;[|apply pf].
Lemma pile_any {Σ : Signature} i:
ProofInfoLe i AnyReasoning.
Tactic Notation "aapply" uconstr(pf)
:= gapply pf; try apply pile_any.
Lemma pile_basic_generic {Σ : Signature} i:
ProofInfoLe BasicReasoning i.
Lemma pile_impl_allows_gen_x {Σ : Signature} x gpi svs kt:
ProofInfoLe ( (ExGen := {[x]}, SVSubst := svs, KT := kt, AKT := false)) ( gpi) →
x ∈ pi_generalized_evars gpi.
Lemma pile_impl_uses_kt {Σ : Signature} gpi evs svs:
ProofInfoLe ( (ExGen := evs, SVSubst := svs, KT := true, AKT := false)) ( gpi) →
pi_uses_kt gpi.
Lemma pile_impl_allows_svsubst_X {Σ : Signature} gpi evs X kt:
ProofInfoLe ( (ExGen := evs, SVSubst := {[X]}, KT := kt, AKT := false)) ( gpi) →
X ∈ pi_substituted_svars gpi.
Lemma liftProofLe {Σ : Signature} (Γ : Theory) (ϕ : Pattern) (i₁ i₂ : ProofInfo)
{pile : ProofLe i₁ i₂}
:
Γ ⊢i ϕ using i₁ →
Γ ⊢i ϕ using i₂.
Lemma liftProofInfoLe {Σ : Signature} (Γ : Theory) (ϕ : Pattern) (i₁ i₂ : ProofInfo)
{pile : ProofInfoLe i₁ i₂}
:
Γ ⊢i ϕ using i₁ →
Γ ⊢i ϕ using i₂.
Tactic Notation "use" constr(i) "in" ident(H) :=
apply liftProofInfoLe with (i₂ := i) in H; [|try_solve_pile].
Close Scope ml_scope.
Import Notations.
Lemma useBasicReasoning {Σ : Signature} {Γ : Theory} {ϕ : Pattern} (i : ProofInfo) :
Γ ⊢i ϕ using BasicReasoning →
Γ ⊢i ϕ using i.
Tactic Notation "remember_constraint" "as" ident(i') :=
match goal with
| [|- (_ ⊢i _ using ?constraint)] ⇒ remember constraint as i'
end.
Lemma useGenericReasoning {Σ : Signature} (Γ : Theory) (ϕ : Pattern) i' i:
(ProofInfoLe i' i) →
Γ ⊢i ϕ using i' →
Γ ⊢i ϕ using i.
Tactic Notation "gapply" uconstr(pf) := eapply useGenericReasoning;[|eapply pf].
Tactic Notation "gapply" uconstr(pf) "in" ident(H) :=
eapply useGenericReasoning in H;[|apply pf].
Lemma pile_any {Σ : Signature} i:
ProofInfoLe i AnyReasoning.
Tactic Notation "aapply" uconstr(pf)
:= gapply pf; try apply pile_any.
Lemma pile_basic_generic {Σ : Signature} i:
ProofInfoLe BasicReasoning i.
Lemma pile_impl_allows_gen_x {Σ : Signature} x gpi svs kt:
ProofInfoLe ( (ExGen := {[x]}, SVSubst := svs, KT := kt, AKT := false)) ( gpi) →
x ∈ pi_generalized_evars gpi.
Lemma pile_impl_uses_kt {Σ : Signature} gpi evs svs:
ProofInfoLe ( (ExGen := evs, SVSubst := svs, KT := true, AKT := false)) ( gpi) →
pi_uses_kt gpi.
Lemma pile_impl_allows_svsubst_X {Σ : Signature} gpi evs X kt:
ProofInfoLe ( (ExGen := evs, SVSubst := {[X]}, KT := kt, AKT := false)) ( gpi) →
X ∈ pi_substituted_svars gpi.
Lemma liftProofLe {Σ : Signature} (Γ : Theory) (ϕ : Pattern) (i₁ i₂ : ProofInfo)
{pile : ProofLe i₁ i₂}
:
Γ ⊢i ϕ using i₁ →
Γ ⊢i ϕ using i₂.
Lemma liftProofInfoLe {Σ : Signature} (Γ : Theory) (ϕ : Pattern) (i₁ i₂ : ProofInfo)
{pile : ProofInfoLe i₁ i₂}
:
Γ ⊢i ϕ using i₁ →
Γ ⊢i ϕ using i₂.
Tactic Notation "use" constr(i) "in" ident(H) :=
apply liftProofInfoLe with (i₂ := i) in H; [|try_solve_pile].
Close Scope ml_scope.
This page has been generated by coqdoc