Fin は構造体だが `constructor` では分解できない

Seasawher commented 3 months ago

/-- 集合の上の全単射の集合 -/
structure Aut (α : Type) where
  map : α → α
  inv : α → α
  leftInv (a : α) : inv (map a) = a
  rightInv (a : α) : map (inv a) = a

-- 置換群
abbrev Perm (n : Nat) := Aut (Fin n)

namespace Perm2

-- Fin は構造体
/-
structure Fin : Nat → Type
number of parameters: 1
constructor:
Fin.mk : {n : Nat} → (val : Nat) → val < n → Fin n
fields:
val : Nat
isLt : ↑self < n
-/
#print Fin

def swap_map : Fin 2 → Fin 2 := fun x => ⟨1 - x.val, by omega⟩

def swap : Perm 2 where
  map := swap_map
  inv := swap_map
  leftInv := by 
    intro a
    -- 失敗する
    fail_if_success constructor
    sorry
  rightInv := by sorry

end Perm2

Seasawher commented 3 months ago

constructor のページで，任意の構造体が分解できると書いてしまったが，誤りかもしれないとりあえず何故うまくいかないのかを知りたい．

Seasawher commented 3 months ago

ゴールの型が Prop だから上手くいかない．当たり前．

lean-ja / lean-by-example

Fin は構造体だが `constructor` では分解できない #332