## Stream: general

### Topic: inherit typeclass instances for a wrapper structure

#### Kris Brown (Aug 07 2020 at 04:49):

Hi, I have a simple wrapper

  @[derive decidable_eq]
structure Address := (val : ℤ)


but want to assign some properties for it already defined for ints (e.g. linear_order) . Is there a straightforward way of defining instances like this beyond duplicating all the code for ints?

#### Yury G. Kudryashov (Aug 07 2020 at 05:40):

We have quite a few defs/lemmas that transfer instances along equivalences.

#### Yury G. Kudryashov (Aug 07 2020 at 05:41):

E.g., look at data/equiv/transfer_instance for algebraic types and docs#linear_order.lift etc for order.

#### Kris Brown (Aug 07 2020 at 06:44):

Thanks, that puts me on track to solve this! It feels basic but I'm going in circles trying to prove the equivalence. I can prove a bijection from int to Address but cannot prove an injection from Address to int, which is what I need

  -- linear_order.lift needs an injective function TO the type that already has
-- a linear_order instance
def cast_address (a:Address): ℤ := a.val

-- needed to prove bij below
lemma val_mk_inverse: ∀ z: Address, (Address.mk z.val) = z := begin
intros, cases z, simp,
end
-- That the inverse of cast_address is surjective might be useful?
lemma bij:  function.bijective Address.mk := begin
unfold function.bijective,
split, {finish}, -- injectivity handled automatically
unfold function.surjective, intros,
have H: Address.mk (b.val) = b := val_mk_inverse  b,
exact ⟨b.val, H⟩
end

lemma inj: function.injective cast_address := begin
unfold function.injective, intros a1 a2 castEq,
unfold cast_address at castEq,
have Hinj: function.injective Address.mk := bij.1,
unfold function.injective at Hinj,

-- have Hsur: function.surjective Address.mk := bij.2,

-- unfold function.surjective at Hsur,

cases Address.decidable_eq a1 a2,

-- have Hsur: function.surjective Address.mk := bij.2,
-- unfold function.surjective at Hsur,
-- have h1 := Hsur a1, have h2 := Hsur a2,
-- cases eq1: h1 with h1v h1', cases eq2: h2 with h2v h2',
-- rw <-h1', rw <-h2', simp,
-- have Hinj: function.injective Address.mk := bij.1,
-- unfold function.injective at Hinj,
-- have Hinj' := @Hinj h1v h2v,
-- apply Hinj',
-- simp,
end


Is there an easy way to do this for a simple wrapper?

#### Kris Brown (Aug 07 2020 at 08:23):

Also not having luck trying to extract the the inverse from the bijection

  def inverse_of_bijection_is_injective: Σ' (f: Address → ℤ), function.injective f :=
-- Error right at the start: "induction tactic failed,
-- recursor 'Exists.dcases_on' can only eliminate into Prop"
match function.bijective_iff_has_inverse.mp bij with
| ⟨a ,b ⟩ := _
end


Different error which I also don't fully grasp when I try this in tactic mode:

  def cast_to_int': Σ' (f: Address → ℤ), function.injective f := begin
have H := function.bijective_iff_has_inverse.mp bij,
existsi H, -- existsi tactic failed, type mismatch between given
--term witness and expected type

end


#### Kevin Buzzard (Aug 07 2020 at 09:42):

You shouldn't be proving things like bijective, you should be writing down functions in each direction and proving they're inverses of each other, ie making a term of type equiv Address int

#### Kevin Buzzard (Aug 07 2020 at 09:45):

To get an inverse operation from a bijection you need the axiom of choice -- why not just build the inverse explicitly and use that

#### Chris Wong (Aug 07 2020 at 10:00):

To explain your error: bijective is defined as a Prop (does not contain data). But Σ is a Type (contains data) and so needs a concrete witness to construct. (Technically your code uses Σ' but the principle is the same.)

#### Kris Brown (Aug 07 2020 at 10:05):

I see now - thanks for explaining the error and connection to choice. And eventually was able to prove the injectivity (don't know why it took me so many attempts):

  structure Address:= (val: ℤ)
def to_z (a:Address): ℤ := a.val

lemma to_z_inj: function.injective to_z := begin
unfold function.injective,
intros  t1 t2 H,
cases e1:t1, cases e2:t2,
simp,unfold to_z at H,
rw e1 at H, rw e2 at H, simp at H, exact H,
end


#### Kevin Buzzard (Aug 07 2020 at 10:42):

The equiv is easier to make and all the lemmas which you're proving are already proved for general equivs.

import tactic

@[derive decidable_eq]
structure Address := (val : ℤ)

def cast_address (a:Address): ℤ := a.val

def inv_fun (n : ℤ) : Address := Address.mk n

def bij : equiv Address ℤ :=
{ to_fun := cast_address,
inv_fun := inv_fun,
left_inv := by {rintro ⟨n⟩, refl },
right_inv := by {intro n, refl } }

lemma val_mk_inverse: ∀ z: Address, (Address.mk z.val) = z := bij.left_inv

lemma bij' :  function.bijective Address.mk := bij.symm.bijective

lemma inj: function.injective cast_address := bij.injective


#### Kevin Buzzard (Aug 07 2020 at 10:43):

If you are in a situation where you can write down the inverse, rather than just abstractly proving that a function is bijective (a weaker statement because it's a Prop rather than data) then you should write down the inverse; it makes your objects much easier to work with.

#### Kenny Lau (Aug 07 2020 at 11:08):

@Kris Brown what do you need this for? (#xy)

#### Kris Brown (Aug 07 2020 at 23:55):

I'll interpret that question pretty broadly. I'm working on a project for formally verified Go code. My initial work was modeling Hoare logic based on this resource (https://github.com/coq-community/hoare-tut) , and lately I've switched to modeling separation logic based on this resource (https://github.com/affeldt-aist/seplog/blob/master/seplog/seplog.v).

I've copied definitions of some of the core data structures to give a feel for the project.

  inductive GoTypeDecl: Type
| gInt:  GoTypeDecl
| gStr:  GoTypeDecl
| gErr:  GoTypeDecl
| gBool: GoTypeDecl
| gPtr:  GoTypeDecl → GoTypeDecl
| gRef:  string → GoTypeDecl

inductive GoPrimType: Type
| pInt:  ℤ  → GoPrimType
| pStr:  string  → GoPrimType
| pErr:  string  → GoPrimType
| pBool: bool → GoPrimType
| pPt: GoTypeDecl → ℤ → GoPrimType
| pStruct' (name : string) (fields : finset string)
(vals : ∀ s ∈ fields, GoPrimType) : GoPrimType

structure GoStruct (name: string):=
(fields: finset string) (vals : ∀ s ∈ fields, GoPrimType)

def type_dict: GoTypeDecl → Type
| gStr    := string
| gErr    := string
| gInt    := ℤ
| gBool   := bool
| (gPtr _):= ℤ
| (gRef s):= GoStruct s

structure Address := (val: ℤ)
structure Heap := (vals: finmap (λ _: Address, Σ dt: GoTypeDecl, type_dict dt))
structure Store :=   (vals: finmap (λ _: string, Σ dt: GoTypeDecl, type_dict dt))
structure Var (t: GoTypeDecl) := (name: string)

inductive Expr: GoTypeDecl → Type
| const  {α: GoTypeDecl}: type_dict α → Expr α
| getvar {α: GoTypeDecl}: Var α → Expr α
| relop {α: GoTypeDecl}:
Relop → Expr α → Expr α → Expr gBool
| binop {α: GoTypeDecl}:
Binop → Expr α → Expr α → Expr α
| unop {α: GoTypeDecl}:
Unop → Expr α → Expr α
| get_field {struct: string} {α: GoTypeDecl}:
Expr (gRef struct) → string → Expr α
| update_field {struct: string} {α: GoTypeDecl}: -- pure update/not mutation
Expr (gRef struct) → string → Expr α → Expr (gRef struct)

inductive cmd: Type
| skip: cmd
| assign   {α: GoTypeDecl}: Var α         → Expr α        → cmd
| lookup   {α: GoTypeDecl}: Var α         → Expr (gPtr α) → cmd
| mutation {α: GoTypeDecl}: Expr (gPtr α) → Expr α        → cmd
| while:                    Expr gBool    → cmd           → cmd
| seq:                      cmd           → cmd           → cmd
| ifte:                     Expr gBool    → cmd           → cmd → cmd
| declare  {α: GoTypeDecl}: Var (gPtr α)  → cmd
| isnil    {α: GoTypeDecl}: Expr (gPtr α) → Var gBool     → cmd
| call {β: GoTypeDecl} {struct: string}
(callee: Expr (gRef struct)) -- object whose method is called
(method: string)             -- Name of method
(arg: list (Σ α, Expr α))    -- Values we want to pass to the func
(result: Var β)              -- store result in this variable
: cmd.

structure Sig :=
(args: list (string × GoTypeDecl))
(return: list (string × GoTypeDecl))
(receiver: string) (is_ptr: bool)

structure GoStructDecl (s:string) :=
(fields: pairmap string GoTypeDecl)
(methods: pairmap string (Sig × cmd))

structure Decls :=
(structs: finmap ((λ s: string, Σ _:unit, GoStructDecl s)))

def Ctx := Store × Heap ×  Decls

-- semantics of expressions
def eval: Π{α: GoTypeDecl}, Expr α → Store → option (type_dict α)
-- Semantics of program commands
inductive exec : option Ctx → cmd → option Ctx → Prop

-- [A bunch of lemmas related to separation logic, weakest preconditions]


To answer the question narrowly, I want to define a to_string method for Heap and I need to convert the map into a list of pairs that can be printed, which requires a decidable linear order on the keys. I could just use raw integers instead of defining Address, but I like the type-safety since integers are used in lots of places.

Last updated: Aug 03 2023 at 10:10 UTC