Skip to content

Commit ccb8361

Browse files
SnO2WMaNCopilot
SnO2WMaN
and
Copilot
committed
some proofs
Co-authored-by: Copilot <copilot@github.com>
0 parents  commit ccb8361

9 files changed

Lines changed: 301 additions & 0 deletions

File tree

‎.github/workflows/lean_action_ci.yml‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
name: Lean Action CI
2+
3+
on:
4+
push:
5+
pull_request:
6+
workflow_dispatch:
7+
8+
jobs:
9+
build:
10+
runs-on: ubuntu-latest
11+
12+
steps:
13+
- uses: actions/checkout@v5
14+
- uses: leanprover/lean-action@v1

‎.gitignore‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
/.lake
2+
3+
# VSCode
4+
.vscode/settings.json

‎Main.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
import SeqPL
2+
3+
def main : IO Unit :=
4+
IO.println s!"Hello, {hello}!"

‎README.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
# SeqPL

‎SeqPL.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
-- This module serves as the root of the `SeqPL` library.
2+
-- Import modules here that should be built as part of the library.
3+
import SeqPL.Basic

‎SeqPL/Basic.lean‎

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
module
2+
3+
public import Mathlib
4+
5+
public section
6+
7+
inductive Formula
8+
| atom : ℕ → Formula
9+
| bot : Formula
10+
| imp : Formula → Formula → Formula
11+
| box : Formula → Formula
12+
deriving Repr, DecidableEq
13+
14+
namespace Formula
15+
16+
prefix:100 "#" => atom
17+
notation:90 "⊥" => bot
18+
infixr:85 " 🡒 " => imp
19+
prefix:95 "□" => box
20+
21+
abbrev neg (A : Formula) : Formula := A 🡒 ⊥
22+
prefix:90 "∼" => neg
23+
24+
abbrev or (A B : Formula) : Formula := ∼A 🡒 B
25+
infixl:83 " ⋎ " => or
26+
27+
abbrev and (A B : Formula) : Formula := ∼(A 🡒 ∼B)
28+
infixl:84 " ⋏ " => and
29+
30+
end Formula
31+
32+
abbrev FormulaFinset := Finset Formula
33+
34+
abbrev FormulaFinset.box (Γ : FormulaFinset) : FormulaFinset := Γ.image (□·)
35+
36+
structure Sequent where
37+
ant : FormulaFinset
38+
suc : FormulaFinset
39+
40+
infix:50 " ⟹ " => Sequent.mk
41+
42+
inductive Proof : Sequent → Type
43+
| axm (A) : Proof ({A} ⟹ {A})
44+
| botL : Proof ({⊥} ⟹ ∅)
45+
| wkL {Γ Γ' Δ} : Proof (Γ ⟹ Δ) → (_ : Γ ⊆ Γ' := by grind) → Proof (Γ' ⟹ Δ)
46+
| wkR {Γ Δ Δ'} : Proof (Γ ⟹ Δ) → (_ : Δ ⊆ Δ' := by grind) → Proof (Γ ⟹ Δ')
47+
| impL {Γ Δ A B} : Proof (Γ ⟹ (insert A Δ)) → Proof (insert B Γ ⟹ Δ) → Proof ((insert (A 🡒 B) Γ) ⟹ Δ)
48+
| impR {Γ Δ A B} : Proof ((insert A Γ) ⟹ (insert B Δ)) → Proof (Γ ⟹ (insert (A 🡒 B) Δ))
49+
| boxGL {Γ A} : Proof ((insert (□A) (Γ ∪ Γ.box)) ⟹ {A}) → Proof (Γ.box ⟹ {□A})
50+
51+
prefix:120 "⊢! " => Proof
52+
53+
namespace Proof
54+
55+
variable {Γ Δ : FormulaFinset} {A B C : Formula}
56+
57+
def union (A) {Γ Δ : Finset _} (hΓ : A ∈ Γ := by grind) (hΔ : A ∈ Δ := by grind) : ⊢! (Γ ⟹ Δ) := wkR $ wkL $ axm A
58+
59+
def botL_mem (h : ⊥ ∈ Γ := by grind) : ⊢! (Γ ⟹ Δ) := wkR (Δ := ∅) $ wkL botL
60+
61+
def mdpL_mem (A B) (h₁ : A 🡒 B ∈ Γ := by grind) (h₂ : A ∈ Γ := by grind) (h₃ : B ∈ Δ := by grind) : ⊢! (Γ ⟹ Δ) := by
62+
rw [(show Γ = insert (A 🡒 B) (insert A (Γ \ {A, A 🡒 B})) by grind)];
63+
apply impL;
64+
. apply union A;
65+
. apply union B;
66+
67+
68+
def negL : ⊢! (Γ ⟹ (insert A Δ)) → ⊢! ((insert (∼A) Γ) ⟹ Δ) := λ p => impL p (wkR $ wkL botL)
69+
70+
def negR : ⊢! ((insert A Γ) ⟹ Δ) → ⊢! (Γ ⟹ (insert (∼A) Δ)) := λ p => impR $ wkR $ wkL p
71+
72+
def andL : ⊢! ((insert A $ insert B $ Γ) ⟹ Δ) → ⊢! (insert (A ⋏ B) Γ ⟹ Δ) := λ p => by
73+
apply impL;
74+
. apply impR;
75+
apply negR;
76+
simpa [(show (insert A $ insert B Γ) = (insert B $ insert A Γ) by grind)] using p;
77+
. exact botL_mem;
78+
79+
def andR : ⊢! (Γ ⟹ insert A Δ) → ⊢! (Γ ⟹ insert B Δ) → ⊢! (Γ ⟹ insert (A ⋏ B) Δ) := λ p q => by
80+
apply impR;
81+
apply impL;
82+
. exact wkR p;
83+
. exact negL $ wkR q;
84+
85+
def orL : ⊢! (insert A Γ ⟹ Δ) → ⊢! (insert B Γ ⟹ Δ) → ⊢! (insert (A ⋎ B) Γ ⟹ Δ) := λ p q => by
86+
apply impL;
87+
. exact negR p;
88+
. exact q;
89+
90+
def orR : ⊢! (Γ ⟹ (insert A $ insert B Δ)) → ⊢! (Γ ⟹ insert (A ⋎ B) Δ) := λ p => by
91+
apply impR;
92+
apply negL;
93+
simpa;
94+
95+
96+
def axiomŁ1 : ⊢! (∅ ⟹ {A 🡒 B 🡒 A}) := impR (Δ := ∅) $ impR $ union A
97+
98+
def axiomŁ2 : ⊢! (∅ ⟹ {(A 🡒 B 🡒 C) 🡒 (A 🡒 B) 🡒 (A 🡒 C)}) := by
99+
apply impR (Δ := ∅);
100+
apply impR;
101+
apply impR;
102+
simp only [insert_empty_eq];
103+
rw [(show {A, A 🡒 B, A 🡒 B 🡒 C} = ({A 🡒 B 🡒 C, A 🡒 B, A}) by grind)];
104+
apply impL;
105+
. exact impL (union A) (union A);
106+
. exact impL (impL (union A) (union B)) (union C);
107+
108+
def axiomŁ3 : ⊢! (∅ ⟹ {(∼A 🡒 ∼B) 🡒 (B 🡒 A)}) := by
109+
apply impR (Δ := ∅);
110+
apply impR;
111+
simp;
112+
rw [(show {B, ∼A 🡒 ∼B} = ({∼A 🡒 ∼B, B}) by grind)];
113+
exact impL (negR $ union A) (negL $ union B);
114+
115+
def axiomK : ⊢! (∅ ⟹ {(□(A 🡒 B) 🡒 (□A 🡒 □B))}) := by
116+
apply impR (Δ := ∅);
117+
apply impR;
118+
simp only [insert_empty_eq];
119+
rw [(show ({□A, □(A 🡒 B)}) = (FormulaFinset.box {A, (A 🡒 B)}) by grind)];
120+
apply boxGL;
121+
apply mdpL_mem A B;
122+
123+
def axiom4 : ⊢! (∅ ⟹ {(□A 🡒 □□A)}) := by
124+
apply impR (Δ := ∅);
125+
simp only [insert_empty_eq];
126+
rw [(show ({□A}) = FormulaFinset.box {A} by grind)];
127+
apply boxGL;
128+
apply union (□A);
129+
130+
def axiomL : ⊢! (∅ ⟹ {□(□A 🡒 A) 🡒 □A}) := by
131+
apply impR (Δ := ∅);
132+
simp only [insert_empty_eq];
133+
rw [(show ({□(□A 🡒 A)}) = FormulaFinset.box {□A 🡒 A} by grind)];
134+
apply boxGL;
135+
apply mdpL_mem (□A) A;
136+
137+
def ruleNec : ⊢! (∅ ⟹ {A}) → ⊢! (∅ ⟹ {□A}) := λ p => boxGL (Γ := ∅) $ wkL p
138+
139+
#eval axiomŁ1 (A := #0) (B := #1)
140+
#eval axiomŁ2 (A := #0) (B := #1) (C := #2)
141+
#eval axiomŁ3 (A := #0) (B := #1)
142+
#eval axiom4 (A := #0)
143+
#eval axiomL (A := #0)
144+
145+
end Proof
146+
147+
148+
149+
abbrev Provable (S : Sequent) : Prop := Nonempty (⊢! S)
150+
prefix:120 "⊢ " => Provable
151+
152+
namespace Provable
153+
154+
variable {Γ Δ : FormulaFinset} {A B C : Formula}
155+
156+
lemma axiomŁ1 : ⊢ (∅ ⟹ {A 🡒 B 🡒 A}) := ⟨Proof.axiomŁ1⟩
157+
lemma axiomŁ2 : ⊢ (∅ ⟹ {(A 🡒 B 🡒 C) 🡒 (A 🡒 B) 🡒 (A 🡒 C)}) := ⟨Proof.axiomŁ2⟩
158+
lemma axiomŁ3 : ⊢ (∅ ⟹ {(∼A 🡒 ∼B) 🡒 (B 🡒 A)}) := ⟨Proof.axiomŁ3⟩
159+
lemma axiomK : ⊢ (∅ ⟹ {(□(A 🡒 B) 🡒 (□A 🡒 □B))}) := ⟨Proof.axiomK⟩
160+
lemma axiom4 : ⊢ (∅ ⟹ {(□A 🡒 □□A)}) := ⟨Proof.axiom4⟩
161+
lemma axiomL : ⊢ (∅ ⟹ {□(□A 🡒 A) 🡒 □A}) := ⟨Proof.axiomL⟩
162+
lemma ruleNec : ⊢ (∅ ⟹ {A}) → ⊢ (∅ ⟹ {□A}) := λ ⟨p⟩ => ⟨Proof.ruleNec p⟩
163+
164+
end Provable

‎lake-manifest.json‎

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
{"version": "1.2.0",
2+
"packagesDir": ".lake/packages",
3+
"packages":
4+
[{"url": "https://github.com/leanprover-community/mathlib4",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "leanprover-community",
8+
"rev": "a529ac800a04d9eb01c671b1f409e965955a58f7",
9+
"name": "mathlib",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "master",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/leanprover-community/plausible",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "leanprover-community",
18+
"rev": "293af9b2a383eed4d04d66b898d608d0a44b750f",
19+
"name": "plausible",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "main",
22+
"inherited": true,
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "leanprover-community",
28+
"rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
29+
"name": "LeanSearchClient",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": "main",
32+
"inherited": true,
33+
"configFile": "lakefile.toml"},
34+
{"url": "https://github.com/leanprover-community/import-graph",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "leanprover-community",
38+
"rev": "fd70b40073aeca8fa60fe0fb492f189d3b12c0ef",
39+
"name": "importGraph",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
42+
"inherited": true,
43+
"configFile": "lakefile.toml"},
44+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "leanprover-community",
48+
"rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
49+
"name": "proofwidgets",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "v0.0.98",
52+
"inherited": true,
53+
"configFile": "lakefile.lean"},
54+
{"url": "https://github.com/leanprover-community/aesop",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "leanprover-community",
58+
"rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5",
59+
"name": "aesop",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "v4.30.0-rc2",
62+
"inherited": true,
63+
"configFile": "lakefile.toml"},
64+
{"url": "https://github.com/leanprover-community/quote4",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "leanprover-community",
68+
"rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809",
69+
"name": "Qq",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "v4.30.0-rc2",
72+
"inherited": true,
73+
"configFile": "lakefile.toml"},
74+
{"url": "https://github.com/leanprover-community/batteries",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11",
79+
"name": "batteries",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "v4.30.0-rc2",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover/lean4-cli",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover",
88+
"rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658",
89+
"name": "Cli",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "v4.30.0-rc2",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"}],
94+
"name": "SeqPL",
95+
"lakeDir": ".lake",
96+
"fixedToolchain": false}

‎lakefile.toml‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
name = "SeqPL"
2+
version = "0.1.0"
3+
defaultTargets = ["seqpl"]
4+
5+
[[lean_lib]]
6+
name = "SeqPL"
7+
8+
[[lean_exe]]
9+
name = "seqpl"
10+
root = "Main"
11+
12+
[[require]]
13+
scope = "leanprover-community"
14+
name = "mathlib"

‎lean-toolchain‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
leanprover/lean4:v4.30.0-rc2

0 commit comments

Comments
 (0)