Grace/Cumulus/Set/Transposition.g17

Open in Workbench Download source

Imports

Involution

Declarations

• exchangedValue defunique
• transposition defgraph
• transposition.first theorem derivation
• transposition.second theorem derivation
• transposition.other theorem derivation
• transposition.involution theorem derivation
• transposition.bijective theorem derivation
• transposition.symmetric theorem derivation
• transposition.conjugate theorem derivation

Source

1-- Exchanging two elements of a set, without Choice.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Set.Transposition8import Involution910defunique exchangedValue (I a b x : Set) (y ∈ I) :=11  (x = a ∧ y = b) ∨ (x = b ∧ y = a) ∨ (x ≠ a ∧ x ≠ b ∧ y = x)12requires ha : a ∈ I13requires hb : b ∈ I14requires member : x ∈ I15proof16  have alternatives : x = a ∨ x = b ∨ (x ≠ a ∧ x ≠ b)17    tauto18  cases alternatives with atFirst | remaining19  . refine ⟨b, hb, ?_⟩20    settle21  . cases remaining with atSecond | outside22    . refine ⟨a, ha, ?_⟩23      settle24    . refine ⟨x, member, ?_⟩25      settle26uniqueness27  intros u hu firstValue v hv secondValue28  cases firstValue with atFirst | remaining29  . cases secondValue with atFirstAgain | other30    . cc31    . cases other with atSecond | outside32      . cc33      . cc34  . cases remaining with atSecond | outside35    . cases secondValue with atFirst | other36      . cc37      . cases other with atSecondAgain | outsideAgain38        . cc39        . cc40    . cases secondValue with atFirst | other41      . cc42      . cases other with atSecond | outsideAgain43        . cc44        . cc4546defgraph transposition (I a b : Set) (x ∈ I) : I := exchangedValue(I, a, b, x)47requires ha : a ∈ I48requires hb : b ∈ I49proof50  have selected := exchangedValue.selected at I, a, b, x with *51  exact selected.left5253section Exchanges54variable (I a b : Set)55hypothesis ha : a ∈ I56hypothesis hb : b ∈ I5758theorem transposition.first59  shows transposition(I, a, b)(a) = b60proof61  have selected := exchangedValue.selected at I, a, b, a with *62  have value := transposition.value at I, a, b, a with *63  have alternatives := selected.right64  cases alternatives with atFirst | remaining65  . cc66  . cases remaining with atSecond | outside67    . cc68    . cc6970theorem transposition.second71  shows transposition(I, a, b)(b) = a72proof73  have selected := exchangedValue.selected at I, a, b, b with *74  have value := transposition.value at I, a, b, b with *75  have alternatives := selected.right76  cases alternatives with atFirst | remaining77  . cc78  . cases remaining with atSecond | outside79    . cc80    . cc8182theorem transposition.other (x : Set)83  requires member : x ∈ I84  requires notFirst : x ≠ a85  requires notSecond : x ≠ b86  shows transposition(I, a, b)(x) = x87proof88  have selected := exchangedValue.selected at I, a, b, x with *89  have value := transposition.value at I, a, b, x with *90  have alternatives := selected.right91  cases alternatives with atFirst | remaining92  . cc93  . cases remaining with atSecond | outside94    . cc95    . cc9697theorem transposition.involution98  shows InvolutionOn(transposition(I, a, b), I)99proof100  have function := transposition.function at I, a, b with *101  have atFirst := transposition.first at I, a, b with *102  have atSecond := transposition.second at I, a, b with *103  unfold InvolutionOn104  refine ⟨function, ?_⟩105  intros x member106  have alternatives : x = a ∨ x = b ∨ (x ≠ a ∧ x ≠ b) by tauto107  cases alternatives with same | remaining108  . cc109  . cases remaining with same | outside110    . cc111    . have unchanged := transposition.other with ha, hb, member, outside.left, outside.right112      cc113114theorem transposition.bijective115  shows BijectiveBetween(transposition(I, a, b), I, I)116proof117  simp [transposition.involution, InvolutionOn.bijective]118119theorem transposition.symmetric120  shows transposition(I, a, b) = transposition(I, b, a)121proof122  have firstFunction := transposition.function at I, a, b with *123  have secondFunction := transposition.function at I, b, a with *124  have firstA := transposition.first at I, a, b with *125  have firstB := transposition.second at I, a, b with *126  have secondA := transposition.second at I, b, a with *127  have secondB := transposition.first at I, b, a with *128  apply FunctionBetween.ext with firstFunction, secondFunction129  intros i member130  have alternatives : i = a ∨ i = b ∨ (i ≠ a ∧ i ≠ b) by tauto131  cases alternatives with atA | rest132  . cc133  . cases rest with atB | outside134    . cc135    . have first := transposition.other with ha, hb, member, outside.left, outside.right136      have second := transposition.other with hb, ha, member, outside.right, outside.left137      cc138139end Exchanges140-- Conjugating (a b) by (b c) gives (a c).141theorem transposition.conjugate (I a b c i : Set)142  requires ha : a ∈ I143  requires hb : b ∈ I144  requires hc : c ∈ I145  requires hi : i ∈ I146  requires ab : a ≠ b147  requires ac : a ≠ c148  requires bc : b ≠ c149  shows transposition(I, b, c)(transposition(I, a, b)(transposition(I, b, c)(i))) = transposition(I, a, c)(i)150proof151  have ba : b ≠ a by simp152  have ca : c ≠ a by simp153  have cb : c ≠ b by simp154  have bcFirst := transposition.first at I, b, c with *155  have bcSecond := transposition.second at I, b, c with *156  have bcOther := transposition.other at I, b, c, a with *157  have abFirst := transposition.first at I, a, b with *158  have abSecond := transposition.second at I, a, b with *159  have abOther := transposition.other at I, a, b, c with *160  have acFirst := transposition.first at I, a, c with *161  have acSecond := transposition.second at I, a, c with *162  have acOther := transposition.other at I, a, c, b with *163  have alternatives : i = a ∨ i = b ∨ i = c ∨ (i ≠ a ∧ i ≠ b ∧ i ≠ c) by tauto164  cases alternatives with first | rest165  . cc166  . cases rest with second | restAgain167    . cc168    . cases restAgain with third | outside169      . cc170      . have outsideBC := transposition.other with hb, hc, hi, outside.right.left, outside.right.right171        have outsideAB := transposition.other with ha, hb, hi, outside.left, outside.right.left172        have outsideAC := transposition.other with ha, hc, hi, outside.left, outside.right.right173        cc174