Zulip Chat Archive

Stream: general

Topic: inherit typeclass instances for a wrapper structure


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Aug 07 2020 at 05:40):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Aug 07 2020 at 11:08):

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

view this post on Zulip 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