File TEST_proofmode_proof_size
From MatchingLogic Require Import Logic
ProofMode.MLPM
Definedness_Syntax.
From Coq Require Import String.
Import
MatchingLogic.Logic.Notations
MatchingLogic.DerivedOperators_Syntax.Notations
.
(* Iterated congruence lemma proved without induction *)
Lemma prf_equiv_congruence_iter_no_ind {Σ : Signature} (Γ : Theory) (p q : Pattern) (C : PatternCtx) l
(wfp : well_formed p)
(wfq : well_formed q)
(wfC : PC_wf C)
(VarsC : pcEvar C ∉ free_evars_of_list l)
(gpi : ProofInfo)
(pile : ProofInfoLe
(ExGen := list_to_set (evar_fresh_seq (free_evars (foldr patt_imp (pcPattern C) l) ∪ 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 (foldr patt_imp (pcPattern C) l) ∪
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
)
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.
Fixpoint proof_size {Σ : Signature} {φ : Pattern} {Γ}
(pf : ML_proof_system Γ φ) : nat :=
match pf with
| ML_Modus_ponens _ phi1 phi2 x x0 ⇒ 1 + proof_size x + proof_size x0
| ML_Ex_gen _ phi1 phi2 x x0 x1 x2 x3 ⇒ 1 + proof_size x2
| ML_Framing_left _ phi1 phi2 psi x x0 ⇒ 1 + proof_size x0
| ML_Framing_right _ phi1 phi2 psi x x0 ⇒ 1 + proof_size x0
| ML_Svar_subst _ phi psi X x x0 x1 ⇒ 1 + proof_size x1
| ML_Knaster_tarski _ phi psi x x0 ⇒ 1 + proof_size x0
| ML_Existence _ ⇒ 1
| _ ⇒ 1
end.
Definition proof_size_info {Σ : Signature} {φ Γ i} (pf : derives_using Γ φ i) : nat :=
match pf with
| exist _ x x0 ⇒ proof_size x
end.
Section compute.
Inductive Symbols :=
| sym_import_definedness (d : Definedness_Syntax.Symbols)
| Zero | Succ (* constructors for Nats *)
| TT | FF
| even
.
Instance Symbols_eqdec : EqDecision Symbols.
#[local]
Program Instance Symbols_fin : Finite Symbols :=
{|
enum := [Zero; Succ; TT ; FF; even;
sym_import_definedness Definedness_Syntax.def_sym] ;
|}.
Instance signature : Signature :=
{| variables := StringMLVariables ;
ml_symbols := {|
symbols := Symbols ;
|} ;
|}.
Instance definedness_syntax : Definedness_Syntax.Syntax :=
{|
Definedness_Syntax.sym_inj := sym_import_definedness;
|}.
Open Scope string_scope.
Open Scope ml_scope.
Let Z := patt_free_evar "Z".
Let X := patt_free_evar "X".
Let Y := patt_free_evar "Y".
Let sym_even := patt_sym even.
Let sym_succ := patt_sym Succ.
Let sym_zero := patt_sym Zero.
Let sym_tt := patt_sym TT.
Let sym_ff := patt_sym FF.
(* axioms *)
Definition defined : Pattern := Definedness_Syntax.axiom AxDefinedness.
(* rewrite example *)
Lemma ex2_pm1 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* example with the induction-based iterated congruence lemma for a smaller context *)
Lemma ex2_pm2 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* example with the complex context-based iterated congruence lemma for a smaller context *)
Lemma ex2_pm3 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* example with the congruence lemma for a smaller context *)
Lemma ex2_pm4 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* These should reflect the idea of mlRewrite: *)
(* Numbers should be similar as for mlRewrite *)
(* example with the induction-based iterated congruence lemma for a bigger context *)
Lemma ex3_pm2 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* example with the complex context-based iterated congruence lemma for a bigger context *)
Lemma ex3_pm3 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* Numbers should be similar as for mlRewrite *)
(* example with the congruence lemma for a big context *)
Lemma ex3_pm4 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
Lemma premise :
∅ ⊢ Y ⋅ Z <---> Y ⋅ Z.
Definition proof_pm1 : nat := proof_size_info (ex2_pm1 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof_pm2 : nat := proof_size_info (ex2_pm2 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof_pm3 : nat := proof_size_info (ex2_pm3 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof_pm4 : nat := proof_size_info (ex2_pm4 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof2_pm2 : nat := proof_size_info (ex3_pm2 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof2_pm3 : nat := proof_size_info (ex3_pm3 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof2_pm4 : nat := proof_size_info (ex3_pm4 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
End compute.
(*
Extraction Language Haskell.
From Coq Require Extraction.
Require Import ExtrHaskellBasic.
Require Import ExtrHaskellString.
Extraction "Test.hs" proof_pm1 proof_pm3 proof_pm2 proof_pm4
proof2_pm3 proof2_pm2 proof2_pm4.
*)
ProofMode.MLPM
Definedness_Syntax.
From Coq Require Import String.
Import
MatchingLogic.Logic.Notations
MatchingLogic.DerivedOperators_Syntax.Notations
.
(* Iterated congruence lemma proved without induction *)
Lemma prf_equiv_congruence_iter_no_ind {Σ : Signature} (Γ : Theory) (p q : Pattern) (C : PatternCtx) l
(wfp : well_formed p)
(wfq : well_formed q)
(wfC : PC_wf C)
(VarsC : pcEvar C ∉ free_evars_of_list l)
(gpi : ProofInfo)
(pile : ProofInfoLe
(ExGen := list_to_set (evar_fresh_seq (free_evars (foldr patt_imp (pcPattern C) l) ∪ 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 (foldr patt_imp (pcPattern C) l) ∪
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
)
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.
Fixpoint proof_size {Σ : Signature} {φ : Pattern} {Γ}
(pf : ML_proof_system Γ φ) : nat :=
match pf with
| ML_Modus_ponens _ phi1 phi2 x x0 ⇒ 1 + proof_size x + proof_size x0
| ML_Ex_gen _ phi1 phi2 x x0 x1 x2 x3 ⇒ 1 + proof_size x2
| ML_Framing_left _ phi1 phi2 psi x x0 ⇒ 1 + proof_size x0
| ML_Framing_right _ phi1 phi2 psi x x0 ⇒ 1 + proof_size x0
| ML_Svar_subst _ phi psi X x x0 x1 ⇒ 1 + proof_size x1
| ML_Knaster_tarski _ phi psi x x0 ⇒ 1 + proof_size x0
| ML_Existence _ ⇒ 1
| _ ⇒ 1
end.
Definition proof_size_info {Σ : Signature} {φ Γ i} (pf : derives_using Γ φ i) : nat :=
match pf with
| exist _ x x0 ⇒ proof_size x
end.
Section compute.
Inductive Symbols :=
| sym_import_definedness (d : Definedness_Syntax.Symbols)
| Zero | Succ (* constructors for Nats *)
| TT | FF
| even
.
Instance Symbols_eqdec : EqDecision Symbols.
#[local]
Program Instance Symbols_fin : Finite Symbols :=
{|
enum := [Zero; Succ; TT ; FF; even;
sym_import_definedness Definedness_Syntax.def_sym] ;
|}.
Instance signature : Signature :=
{| variables := StringMLVariables ;
ml_symbols := {|
symbols := Symbols ;
|} ;
|}.
Instance definedness_syntax : Definedness_Syntax.Syntax :=
{|
Definedness_Syntax.sym_inj := sym_import_definedness;
|}.
Open Scope string_scope.
Open Scope ml_scope.
Let Z := patt_free_evar "Z".
Let X := patt_free_evar "X".
Let Y := patt_free_evar "Y".
Let sym_even := patt_sym even.
Let sym_succ := patt_sym Succ.
Let sym_zero := patt_sym Zero.
Let sym_tt := patt_sym TT.
Let sym_ff := patt_sym FF.
(* axioms *)
Definition defined : Pattern := Definedness_Syntax.axiom AxDefinedness.
(* rewrite example *)
Lemma ex2_pm1 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* example with the induction-based iterated congruence lemma for a smaller context *)
Lemma ex2_pm2 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* example with the complex context-based iterated congruence lemma for a smaller context *)
Lemma ex2_pm3 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* example with the congruence lemma for a smaller context *)
Lemma ex2_pm4 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* These should reflect the idea of mlRewrite: *)
(* Numbers should be similar as for mlRewrite *)
(* example with the induction-based iterated congruence lemma for a bigger context *)
Lemma ex3_pm2 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* example with the complex context-based iterated congruence lemma for a bigger context *)
Lemma ex3_pm3 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
(* Numbers should be similar as for mlRewrite *)
(* example with the congruence lemma for a big context *)
Lemma ex3_pm4 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
well_formed (A ---> B ---> C ---> D) = true →
Γ ⊢ ((B ⋅ C) <---> D) →
Γ ⊢ A ---> ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.
Lemma premise :
∅ ⊢ Y ⋅ Z <---> Y ⋅ Z.
Definition proof_pm1 : nat := proof_size_info (ex2_pm1 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof_pm2 : nat := proof_size_info (ex2_pm2 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof_pm3 : nat := proof_size_info (ex2_pm3 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof_pm4 : nat := proof_size_info (ex2_pm4 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof2_pm2 : nat := proof_size_info (ex3_pm2 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof2_pm3 : nat := proof_size_info (ex3_pm3 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
Definition proof2_pm4 : nat := proof_size_info (ex3_pm4 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise).
End compute.
(*
Extraction Language Haskell.
From Coq Require Extraction.
Require Import ExtrHaskellBasic.
Require Import ExtrHaskellString.
Extraction "Test.hs" proof_pm1 proof_pm3 proof_pm2 proof_pm4
proof2_pm3 proof2_pm2 proof2_pm4.
*)
This page has been generated by coqdoc