Created
December 1, 2024 14:47
-
-
Save andrejbauer/0522b62e85dc13b205e70b00e21e694d to your computer and use it in GitHub Desktop.
A formalization of a classical propositional calculus used in some questions and answers at ProofAssistants StackExchange
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* A formalization of a classical propositional calculus a la user4035, | |
see https://proofassistants.stackexchange.com/q/4443/169 and | |
https://proofassistants.stackexchange.com/q/4468/169 , | |
with the following modifications: | |
1) We use a set of assumptions rather than a list of assumptions. | |
2) We use derivation trees to represent proofs instead of lists of formulas. | |
Proofs-as-lists are used in Hilbert-style systems, whereas | |
derivation trees are more common in natural-deduction style rules. | |
The present formalization is a bit of a mix: the axioms and rules | |
are those of a Hulbert-style system, but derivations are not linearized | |
into lists. I think it is fair to still call this a mostly-Hilbert-style | |
system. | |
*) | |
(* Atomic proposition. *) | |
Parameter atom : Set. | |
(* We assume atomic propositions form a set with decidable equality. *) | |
Parameter atom_eq : forall (a b : atom), {a = b} + {a <> b}. | |
(* Propositional formulas *) | |
Inductive formula : Type := | |
| f_atom : atom -> formula | |
| f_not : formula -> formula | |
| f_imp : formula -> formula -> formula. | |
Notation "- F" := (f_not F) (at level 35, right associativity). | |
Notation "F ~> G" := (f_imp F G) (at level 45, right associativity). | |
(* Equality of formulas is decidable. *) | |
Lemma formula_eq (A B : formula) : {A = B} + {A <> B}. | |
Proof. | |
decide equality. | |
now apply atom_eq. | |
Qed. | |
(* Instead of working with lists of assumptions we shall work with | |
sets of assumptions. A set of formulas can be represented by its | |
characteristic map formula -> Prop. *) | |
(* Element-hood relation between a formula and a set of formulas. *) | |
Definition elem (A : formula) (Γ : formula -> Prop) := Γ A. | |
Infix "∈" := elem (at level 50). | |
(* The empty context. *) | |
Definition empty : formula -> Prop := fun _ => False. | |
(* The union of two sets of formulas. *) | |
Definition union (Γ Δ : formula -> Prop) A := A ∈ Γ \/ A ∈ Δ. | |
Infix "∪" := union (at level 61, left associativity). | |
(* The subset relation between sets of formulas. *) | |
Definition subset (Γ Δ : formula -> Prop) := | |
forall A, A ∈ Γ -> A ∈ Δ. | |
Infix "⊆" := subset (at level 71). | |
(* We now come to main definitions. We first define a type | |
Γ |- A whose elements are derivations of formula A | |
from assumptions Γ. These are presented as derivation trees, | |
rather than more traditional lists. | |
Note the difference between declaring that Γ |- A | |
is a Prop vs. a Type: | |
- if Γ |- A is a Prop, then it is expresses *provability* | |
- if Γ |- A is a Type, then it expresses *proof derivations* | |
The practical difference is this: if Γ |- A is a Type, then | |
its element is a derivation tree which can be freely inspected | |
and used; but if Γ |- A is a Prop, then its elements are | |
(abstract) witnesses of provability that can only be expected | |
for the purpose of constructing an element of Prop. | |
*) | |
Reserved Notation "Γ |- A" (at level 98). | |
Inductive entails (Γ : formula -> Prop) : formula -> Type := | |
| hypo : forall A, A ∈ Γ -> Γ |- A (* every hypothesis is provable *) | |
| axiom1 : forall A B , Γ |- A ~> B ~> A | |
| axiom2 : forall A B C, Γ |- (A ~> B ~> C) ~> (A ~> B) ~> (A ~> C) | |
| axiom3 : forall A B, Γ |- (- B ~> - A) ~> (- B ~> A) ~> B | |
| mp : forall A B, Γ |- B -> Γ |- B ~> A -> Γ |- A (* modus ponens *) | |
where "Γ |- A" := (entails Γ A). | |
(* It is convenient to make some parameters implicit. *) | |
Arguments hypo {_} {_} _. | |
Arguments axiom1 {_} _ _. | |
Arguments axiom2 {_} _ _ _. | |
Arguments axiom3 {_} _ _. | |
Arguments mp {_} {_} (_). | |
(* Here are some basic observation about |-. *) | |
Lemma imply_self Γ A : Γ |- A ~> A. | |
Proof. | |
apply (mp (A ~> A ~> A)). | |
- apply axiom1. | |
- apply (mp ((A ~> (A ~> A) ~> A))). | |
+ apply axiom1. | |
+ apply axiom2. | |
Defined. | |
(* We can inspect proofs by telling Coq to compute the normal form. | |
For example, here is how we can see the proof constructed in | |
the previous lemma. *) | |
Eval compute in (fun A => (imply_self empty A)). | |
(* output: | |
= fun A : formula => | |
mp (A ~> A ~> A) | |
(axiom1 A A) | |
(mp (A ~> (A ~> A) ~> A) | |
(axiom1 A (A ~> A)) | |
(axiom2 A (A ~> A) A)) | |
: forall A : formula, empty |- A ~> A | |
*) | |
(* Weakening: having more hypotheses does not hurt. *) | |
Theorem weaken Γ Δ A : Γ ⊆ Δ -> Γ |- A -> Δ |- A. | |
Proof. | |
intros S H. | |
induction H as [B ?|?|?|?|C D K L IH1 IH2]. | |
- now apply hypo, S. | |
- apply axiom1. | |
- apply axiom2. | |
- apply axiom3. | |
- now apply mp with (B := D). | |
Qed. | |
(* "extend Γ A" is the set Γ ∪ {A}. *) | |
Definition extend Γ A := fun B => B ∈ Γ \/ A = B. | |
Notation "Γ ,, A" := (extend Γ A) (at level 32, left associativity). | |
(* The cut rule is admissible. *) | |
Theorem CutRule A {Γ B} : Γ |- A -> extend Γ A |- B -> Γ |- B. | |
Proof. | |
intros H G. | |
induction G as [B L|?|?|?|?]. | |
- destruct (formula_eq A B) as [[]|N]. | |
+ assumption. | |
+ apply hypo. | |
now destruct L as [|]. | |
- apply axiom1. | |
- apply axiom2. | |
- apply axiom3. | |
- now apply (mp B). | |
Qed. | |
(* We need this lemma in the deduction theorem. *) | |
Lemma drop_antecedent Γ A B : Γ |- B -> Γ |- A ~> B. | |
Proof. | |
intro H. | |
apply (mp B). | |
- assumption. | |
- apply axiom1. | |
Qed. | |
(* We conclude with the proof of the deduction theorem, just to show | |
that it is quite painless to formalize. *) | |
Theorem deduction {Γ A B} : extend Γ A |- B -> Γ |- A ~> B. | |
Proof. | |
intro H. | |
induction H as [B G|?|?|?|C]. | |
- destruct (formula_eq A B) as [[]|N]. | |
+ apply imply_self. | |
+ apply mp with (B := B). | |
* apply hypo. | |
now destruct G as [|]. | |
* apply axiom1. | |
- apply drop_antecedent. | |
apply axiom1. | |
- apply drop_antecedent. | |
apply axiom2. | |
- apply drop_antecedent. | |
apply axiom3. | |
- apply (mp (A ~> B)). | |
+ assumption. | |
+ apply (mp (A ~> B ~> C)). | |
* assumption. | |
* apply axiom2. | |
Qed. | |
(* We give three versions of deducing A ~> B, B ~> C |- A ~> C. | |
It is easier and more general to show the statement: | |
if (A ~> B) ∈ Γ and (B ~> C) ∈ Γ then Γ |- A ~> C. | |
*) | |
(* The first version is the most explicit one, but it requires us | |
to use "or_intror" and "or_introl" with bare hands. *) | |
Theorem example1 Γ A B C (H1 : A ~> B ∈ Γ) (H2 : B ~> C ∈ Γ) : | |
Γ |- A ~> C. | |
Proof. | |
apply deduction. | |
apply (mp B). | |
- apply (mp A). | |
* apply (hypo (or_intror eq_refl)). | |
* apply (hypo (or_introl H1)). | |
- apply (hypo (or_introl H2)). | |
Qed. | |
(* Same as above, but with tactics "left" and "right" instead of manual | |
use of "or_introl" and "or_intror". *) | |
Theorem example2 Γ A B C (H1 : A ~> B ∈ Γ) (H2 : B ~> C ∈ Γ) : | |
Γ |- A ~> C. | |
Proof. | |
apply deduction. | |
apply (mp B). | |
- apply (mp A). | |
* apply hypo. now right. | |
* apply hypo. now left. | |
- apply hypo. now left. | |
Qed. | |
(* Ideally we would like a tactic that can solve easy cases of "hypo", | |
but the previous proof is not amenable to an easy such tactic because | |
we directed Coq using "left" and "right". Here is another proof, | |
where all cases of "hypo" are solved the same way. *) | |
Theorem example3 Γ A B C (H1 : A ~> B ∈ Γ) (H2 : B ~> C ∈ Γ) : | |
Γ |- A ~> C. | |
Proof. | |
apply deduction. | |
apply (mp B). | |
- apply (mp A). | |
* apply hypo. unfold extend, elem. auto. | |
* apply hypo. unfold extend, elem. auto. | |
- apply hypo. unfold extend, elem. auto. | |
Qed. | |
(* Now we can define a tactic that does the above steps. | |
Note the difference between the tactic "hypo" and the constructor "hypo"! | |
If you type "hypo" in tactic mode, it will use the tactic defined below, | |
but if you type "apply hypo" it will use the constructor hypo. *) | |
Ltac hypo := (apply hypo ; unfold extend, elem ; auto). | |
(* The final version. *) | |
Theorem example4 Γ A B C (H1 : A ~> B ∈ Γ) (H2 : B ~> C ∈ Γ) : | |
Γ |- A ~> C. | |
Proof. | |
apply deduction. | |
apply (mp B). | |
- apply (mp A) ; hypo. | |
- hypo. | |
Qed. | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment