Examples.lean

1 import ProofPath.Field
2 import ProofPath.Protected
3 import ProofPath.Compression
4 import Mathlib.Tactic.FinCases
5 
6 namespace ProofPath.Examples
7 
8 /-- One conjunction needs both premises. No provenance tag changes this. -/
9 def conjunctionField : Field (Fin 3) Unit where
10   leaf := ∅
11   premises _ := {v | v ≠ 2}
12   conclusion _ := 2
13   certified _ := True
14 
15 def pairPatch (i : Bool) : Set (Fin 3) :=
16   if i then {1, 2} else {0, 2}
17 
18 def pairLocal (i : Bool) : conjunctionField.Local (pairPatch i) where
19   val v := v ∈ pairPatch i ∧ v ≠ 2
20   outside := fun _ hv h => hv h.1
21   leaves := by intro v hv; simp [conjunctionField] at hv
22   rules := by
23     intro j _ hs _
24     cases i
25     · have h := hs (by simp [Field.support, conjunctionField] : (1 : Fin 3) ∈ conjunctionField.support j)
26       simp [pairPatch] at h
27     · have h := hs (by simp [Field.support, conjunctionField] : (0 : Fin 3) ∈ conjunctionField.support j)
28       simp [pairPatch] at h
29 
30 theorem pairwise_data_match : conjunctionField.Matching pairPatch pairLocal := by
31   intro i j v hi hj
32   exact ⟨fun h => ⟨hj, h.2⟩, fun h => ⟨hi, h.2⟩⟩
33 
34 theorem pairwise_patches_cover : ∀ v, ∃ i, v ∈ pairPatch i := by
35   intro v
36   fin_cases v
37   · exact ⟨false, by simp [pairPatch]⟩
38   · exact ⟨true, by simp [pairPatch]⟩
39   · exact ⟨false, by simp [pairPatch]⟩
40 
41 theorem pairwise_data_have_no_glue :
42     ¬ ∃ x, conjunctionField.Model x ∧
43       ∀ i v, v ∈ pairPatch i → (x v ↔ (pairLocal i).val v) := by
44   rintro ⟨x, hx, ha⟩
45   have h0 : x 0 := (ha false 0 (by simp [pairPatch])).mpr (by simp [pairPatch, pairLocal])
46   have h1 : x 1 := (ha true 1 (by simp [pairPatch])).mpr (by simp [pairPatch, pairLocal])
47   have hn2 : ¬ x 2 := fun h => (by simp [pairLocal] : ¬ (pairLocal false).val 2)
48     ((ha false 2 (by simp [pairPatch])).mp h)
49   apply hn2
50   apply hx.2 () trivial
51   intro v hv
52   fin_cases v
53   · exact h0
54   · exact h1
55   · exact False.elim (hv rfl)
56 
57 /-- A zero residual is not evidence of preserving the requested data. -/
58 theorem rigid_obstruction :
59     ¬ ∃ y : ℚ, (LinearMap.id : ℚ →ₗ[ℚ] ℚ) y = 0 ∧
60       (LinearMap.id : ℚ →ₗ[ℚ] ℚ) y = (1 : ℚ) := by
61   rintro ⟨y, h0, h1⟩
62   exact (zero_ne_one : (0 : ℚ) ≠ 1) (h0.symm.trans h1)
63 
64 end ProofPath.Examples

Back to source controls