Skip to content

Proof of PNNetwork.boxProd preserving SimplePN #16

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
chi-p-3141 wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Proof of PNNetwork.boxProd preserving SimplePN #16

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
91425d8
proved boxProd preserves SimplePN
chi-p-3141 Apr 14, 2026
3fc8fa9
edited proof for length/readability
chi-p-3141 Apr 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
64 changes: 63 additions & 1 deletion DGAlgorithms/Network/PNNetwork.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -448,7 +448,69 @@ def PNNetwork.boxProd (G : PNNetwork V) (G' : PNNetwork V') : PNNetwork (V × V'
/-- Box product of PNNetworks. -/
infixl:70 " □ " => PNNetwork.boxProd

-- instance (G : PNNetwork V) (G' : PNNetwork V') [SimplePN G] [SimplePN G'] : SimplePN (G □ G') := sorry
instance (G : PNNetwork V) (G' : PNNetwork V') [hg : SimplePN G] [hg': SimplePN G'] : SimplePN (G □ G') := by
constructor
-- loopless
Comment on lines +452 to +453
Copy link
Copy Markdown
Owner

@Shreyas4991 Shreyas4991 Apr 14, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When starting a case analysis using cases or constructors, you should use the case selector notation. For constructor, by_cases, split, and split_ifs, the . case selector is preferred although you can also use case <case name from goal state> <additional variable introduced in this case> => proof. For cases .. with and induction .. with I suggest using the code action that vscode shows (keyboard shortcut : Ctrl + . and letting it create the arms of the proof for you. In either case the proof of the case is indented more than the proof outside. Similarly proofs of haves should have an extra indentation to clearly show that they are proofs of the have statements.

intro (v1,v2) k1 k2 k1_valid absurd
cases heq1 : unpair (G.deg v1) (G'.deg v2) k1 with
| mk a1 b1
let ⟨a1_valid,b1_valid⟩ := unpair_valid k1 k1_valid
simp [heq1] at a1_valid b1_valid
cases heq2 : unpair (G.deg v1) (G'.deg v2) k2 with
| mk a2 b2
unfold unpair at heq1 heq2
unfold PNNetwork.boxProd at k1_valid
simp [k1_valid] at heq1
have k2_valid : (k2 < (G □ G').deg (v1,v2)) := by
have rwrt : (k2 = ((v1, v2), k2).2) := rfl
have involution : ((G □ G').pmap ((v1, v2), k2) = ((v1, v2), k1)) := by
rw [← absurd, (G □ G').pmap_involutive]
exact k1_valid
rw [rwrt]
apply (G □ G').is_well_defined ((v1, v2), k2)
rw [involution]
exact k1_valid
unfold PNNetwork.boxProd at k2_valid
simp [k2_valid] at heq2
simp at k1_valid
have gdegpos : (0 < G.deg v1) := by nlinarith
apply hg.loopless v1 a1 a2
exact a1_valid
simp [PNNetwork.boxProd, unpair, pair, k1_valid, heq1.left, heq1.right,Port.port, Port.node] at absurd
let ⟨⟨abs1, abs2⟩, abs3⟩ := absurd
apply Prod.ext
exact abs1
simp [a1_valid, b1_valid,abs1] at abs3
have hyp : (k2 % (G.deg v1)=(G.pmap (v1,a1)).2) := by
rw [← abs3, mul_comm, Nat.mul_add_mod (G.deg v1) ((G'.pmap (v2,b1)).2) ((G.pmap (v1,a1)).2)]
apply Nat.mod_eq_of_lt
let lem := (G.is_well_defined_iff (v1,a1)).mpr
dsimp [PNNetwork.PortValid, Port.port, Port.node] at lem
simp [abs1] at lem
exact lem a1_valid
simp
rw [← hyp]
exact heq2.left
-- simple
intro (v1,v2) k1 k2 k1_valid k2_valid
cases heq1 : unpair (G.deg v1) (G'.deg v2) k1 with
| mk a1 b1
let ⟨a1_valid, b1_valid⟩ := unpair_valid k1 k1_valid
simp [heq1] at a1_valid b1_valid
cases heq2 : unpair (G.deg v1) (G'.deg v2) k2 with
| mk a2 b2
let ⟨a2_valid, b2_valid⟩ := unpair_valid k2 k2_valid
simp [heq2] at a2_valid b2_valid
simp [PNNetwork.boxProd, heq1, heq2, Port.node]
intro heqa heqb
let a1_eq_a2 := hg.simple v1 a1 a2 a1_valid a2_valid heqa
let b1_eq_b2 := hg'.simple v2 b1 b2 b1_valid b2_valid heqb
dsimp [unpair, PNNetwork.boxProd] at *
simp [k1_valid] at heq1
simp [k2_valid] at heq2
rw [← Nat.div_add_mod k1 (G.deg v1), ← Nat.div_add_mod k2 (G.deg v1), heq1.left, heq1.right, heq2.left, heq2.right, a1_eq_a2, b1_eq_b2]



-- lemma box_prod_comm (G : PNNetwork V) (G' : PNNetwork V') [SimplePN G] [SimplePN G'] : (G □ G').to_SimpleGraph = (G.to_SimpleGraph □ G'.to_SimpleGraph) := by
-- ext v v'
Expand Down