# Zulip Chat Archive

## 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 `def`

s/`lemma`

s 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 `equiv`

s.

```
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: May 10 2021 at 00:31 UTC