From 3c9b548bf9efe37f7f569673b32a556e7ca97805 Mon Sep 17 00:00:00 2001 From: Mark Koch Date: Sun, 9 Jun 2024 12:33:32 +0100 Subject: [PATCH] Fix theory support in Proof Mode --- theories/Proofmode/DemoPA.v | 31 +++++++++++++++++++++++++++++++ theories/Proofmode/ProofMode.v | 34 +++++++++++++++++----------------- theories/Proofmode/Theories.v | 10 +++++----- 3 files changed, 53 insertions(+), 22 deletions(-) diff --git a/theories/Proofmode/DemoPA.v b/theories/Proofmode/DemoPA.v index 89cb322f..4c9f4737 100644 --- a/theories/Proofmode/DemoPA.v +++ b/theories/Proofmode/DemoPA.v @@ -75,6 +75,37 @@ Proof. Qed. +(* The same also works in theories *) + +Definition FAeqT phi := In phi FAeq. + +Goal forall T a b c, T ⊩ (a → (a → b) → (b → c) → c). +Proof. + intros. fstart. fintros. fapply "H1". fapply "H0". fapply "H". +Qed. + +Lemma num_add_homomorphism_T x y : + FAeqT ⊩ (num x ⊕ num y == num (x + y)). +Proof. + induction x; cbn. + - fapply ax_add_zero. (* Arguments are infered! *) + - feapply ax_trans. + + fapply ax_add_rec. + + feapply ax_succ_congr. exact IHx. +Qed. + +Lemma num_mult_homomorphism_T x y : + FAeqT ⊩ ( num x ⊗ num y == num (x * y) ). +Proof. + induction x; cbn. + - fapply ax_mult_zero. + - feapply ax_trans. + + feapply ax_trans. + * fapply ax_mult_rec. + * feapply ax_add_congr. fapply ax_refl. exact IHx. + + apply num_add_homomorphism_T. +Qed. + (* Setup rewriting *) diff --git a/theories/Proofmode/ProofMode.v b/theories/Proofmode/ProofMode.v index a4df5a93..35cf3cb4 100644 --- a/theories/Proofmode/ProofMode.v +++ b/theories/Proofmode/ProofMode.v @@ -137,12 +137,12 @@ Instance prv_WeakClass `{funcs_signature, preds_signature, falsity_flag, peirce} (* TODO: Why doesn't this exist? *) #[global] -Instance eq_dec_full_operators : eq_dec binop. unfold dec; decide equality. Qed. +Instance eq_dec_full_operators : EqDec binop. unfold EqDec, dec; decide equality. Qed. #[global] -Instance eq_dec_full_logic_quant : eq_dec quantop. unfold dec; decide equality. Qed. +Instance eq_dec_full_logic_quant : EqDec quantop. unfold EqDec, dec; decide equality. Qed. #[global] -Instance tprv_DeductionRules `{funcs_signature, preds_signature, falsity_flag, peirce, eq_dec syms, eq_dec preds} : DeductionRules theory tprv (fun a b => extend b a) mapT (fun a b => in_theory b a) := +Instance tprv_DeductionRules `{funcs_signature, preds_signature, falsity_flag, peirce, EqDec syms, EqDec preds} : DeductionRules theory tprv (fun a b => extend b a) mapT (fun a b => in_theory b a) := {| II := Theories.T_II ; IE := Theories.T_IE ; @@ -476,11 +476,11 @@ Ltac make_compatible tac := | _ => idtac end; try update_binder_names (* [try] because some tactics add normal Coq goals *) - | [ |- @tpm _ _ ?p ?C _ ] => + | [ |- @tpm _ _ _ ?p ?C _ ] => fstop; tac C; match goal with - | [ |- tprv _ ?G ] => change (@tpm _ _ p C G) + | [ |- tprv _ ?G ] => change (@tpm _ _ _ p C G) | _ => idtac end; try update_binder_names (* [try] because some tactics add normal Coq goals *) @@ -500,11 +500,11 @@ Ltac make_compatible_light tac := | [ |- prv _ ?G ] => change (@pm _ _ _ p C G) | _ => idtac end - | [ |- @tpm _ _ ?p ?C _ ] => + | [ |- @tpm _ _ _ ?p ?C _ ] => fstop; tac C; match goal with - | [ |- tprv _ ?G ] => change (@tpm _ _ p C G) + | [ |- tprv _ ?G ] => change (@tpm _ _ _ p C G) | _ => idtac end end. @@ -815,8 +815,8 @@ Section Fintro. eapply Weak in Ht. eapply IE. apply Ht. ctx. firstorder. Qed. - Context {eq_dec_Funcs : eq_dec syms}. - Context {eq_dec_Preds : eq_dec preds}. + Context {eq_dec_Funcs : EqDec syms}. + Context {eq_dec_Preds : EqDec preds}. Lemma intro_and_destruct_T T s t G : T ⊩ (s → t → G) -> T ⊩ (s ∧ t → G). @@ -1211,8 +1211,8 @@ Section Fapply. intros. apply (IE (phi := psi)). eapply CE2. apply H. apply H0. Qed. - Context {eq_dec_Funcs : eq_dec syms}. - Context {eq_dec_Preds : eq_dec preds}. + Context {eq_dec_Funcs : EqDec syms}. + Context {eq_dec_Preds : EqDec preds}. Lemma fapply_equiv_l_T A phi psi : A ⊩ (phi ↔ psi) -> A ⊩ phi -> A ⊩ psi. @@ -1497,8 +1497,8 @@ Section Fassert. intros H1 H2. eapply IE. exact H2. exact H1. Qed. - Context {eq_dec_Funcs : eq_dec syms}. - Context {eq_dec_Preds : eq_dec preds}. + Context {eq_dec_Funcs : EqDec syms}. + Context {eq_dec_Preds : EqDec preds}. Lemma fassert_help_T `{peirce} A phi psi : A ⊩ phi -> A ⊩ (phi → psi) -> A ⊩ psi. @@ -1585,8 +1585,8 @@ Section Fdestruct. intros H1 H2. fintros. fapply H2. fapply 0. eapply Weak. apply H1. firstorder. Qed. - Context {eq_dec_Funcs : eq_dec syms}. - Context {eq_dec_Preds : eq_dec preds}. + Context {eq_dec_Funcs : EqDec syms}. + Context {eq_dec_Preds : EqDec preds}. Lemma fdestruct_discharge_premises_T T a b c : T ⊩ a -> T ⊩ (b → c) -> T ⊩ ((a → b) → c). @@ -1720,8 +1720,8 @@ Section Classical. apply Ctx. now left. Qed. - Context {eq_dec_Funcs : eq_dec syms}. - Context {eq_dec_Preds : eq_dec preds}. + Context {eq_dec_Funcs : EqDec syms}. + Context {eq_dec_Preds : EqDec preds}. Lemma case_help_T A phi psi : A ⊩C (phi ∨ (phi → ⊥) → psi) -> A ⊩C psi. diff --git a/theories/Proofmode/Theories.v b/theories/Proofmode/Theories.v index 5447989b..97264dd7 100644 --- a/theories/Proofmode/Theories.v +++ b/theories/Proofmode/Theories.v @@ -45,12 +45,12 @@ Context {p : peirce}. Definition mapT (f : form -> form) (T : theory) : theory := fun phi => exists psi, T psi /\ f psi = phi. -Context {eq_dec_Funcs : eq_dec syms}. -Context {eq_dec_Preds : eq_dec preds}. -Context {eq_dec_binop : eq_dec binop}. -Context {eq_dec_quantop : eq_dec quantop}. +Context {eq_dec_Funcs : EqDec syms}. +Context {eq_dec_Preds : EqDec preds}. +Context {eq_dec_binop : EqDec binop}. +Context {eq_dec_quantop : EqDec quantop}. -Definition rem := @remove form (dec_form _ _ _ _). +Definition rem := @remove form (dec_form eq_dec_Funcs eq_dec_Preds eq_dec_binop eq_dec_quantop). Theorem WeakT A B phi :