deriving lift/coe for structure members.

Stream: new members

[Ocschwar]

I have to do some math with \nat and \int members of a structure:

@[derive inhabited ]
structure position :=
(distance : ℕ)
(depth : ℕ)
(aim : ℤ )
 ```
and I am unable to lift from one set to the other.:

((position.aim p) * (instruction.length i))

gets me "type mismatch at application
  has_mul.mul p.aim
term
  p.aim
has type
  ℤ
but is expected to have type
  ℕ"

All attempts to lift members of the expression are failing. Do I need to derive something with the structures first>?

[Kyle Miller]

The answer to this depends on the context of this expression. A #mwe could be helpful.

If you know the result is supposed to be an integer, you could do (position.aim p) * (instruction.length i : ℤ).

[Ocschwar]

This is it: https://github.com/ocschwar/adventofcode/blob/master/src/aoc/day2.lean
I can drill it down too

[Ocschwar]

import init.data.nat
import init.data.to_string
import data.set
import data.list.basic
import data.bool
import data.buffer.parser
#check prod.mk
open parser
open io

@[derive  inhabited ]
structure position :=
(distance : ℕ)
(depth : ℕ)
(aim : ℤ )
@[derive inhabited]
inductive comd : Type
| up : comd
| down : comd
| forward : comd
@[derive inhabited]
structure instruction :=
(comd : comd )
(length : ℕ  )


def mkstr  (p:position): string :=
  (to_string (position.depth p)) ++ ", "  ++ to_string(position.distance p)


def move_position (p:position) (i:instruction ) : position :=
  position.mk ((position.distance p)+
  (match (instruction.comd i) with
     comd.forward :=  ↑  ( instruction.length i)  ,
     comd.up := 0 ,
     comd.down := 0
  end
  ))
  (0 +
   (match (instruction.comd i) with
     comd.forward :=  match cmp (position.aim p) 0 with
     | ordering.eq := 0
     | ordering.gt := (position.depth p )+ ((position.aim p) * (instruction.length i:ℤ ))
     | ordering.lt := (match (position.depth p) ((-position.aim p) * (instruction.length i)) with
        |ordering.gt := 0
        | ordering.eq := 0
        | ordering.lt := 0
        end )
      end
      |comd.up:= 0
      |comd.down:= 0
      end))
      (match (instruction.comd i) with
      | comd.forward := (position.aim p )
      | comd.up := (position.aim p)+ (instruction.length i)
      | comd.down := (position.aim p)- (instruction.length i))

[Eric Wieser]

It won't fix your issue, but instead of position.mk _ _ _ I recommend { distance := _, depth := _, aim := _ }

[Ocschwar]

Definitely looks more ergonomic. I'll switch

[Eric Wieser]

The error message above is telling you "you're trying to convert an int into a nat", probably because you're trying to set depth to an int calculation

[Ocschwar]

I am, because depth is a depth in water dimension, so the negative is meaningless. I thought setting it to a nat will be a succinct way of enforcing depth to be non-negative.

[Eric Wieser]

Right, but what if the thing you try to assign to it is negative?

[Eric Wieser]

Do you want the absolute value? The truncation?

[Eric Wieser]

Which line in the above code is the one that fails?

[Kevin Buzzard]

Right now, whether you mean to or not, you have an integer and are trying to pretend that it's a natural, and Lean knows that this is impossible. But it's hard for people to explain to you how you've done this and how to fix it because we can't see the error happening on our own machines.

[Kevin Buzzard]

     | ordering.gt := (position.depth p )+ ((position.aim p) * (instruction.length i:ℤ ))

->

type mismatch at application
  has_mul.mul p.aim
term
  p.aim
has type
  ℤ
but is expected to have type
  ℕ

[Kevin Buzzard]

What's happening here is that you want seem to be trying to define a number of the form A+(B*C). Lean takes a look at A and sees it's a natural, concludes that + must indicate addition of naturals, that B * C is a natural, that * is multiplication of naturals, and that B must be a natural, and then it discovers that B is an integer. Hence the error.

[Kevin Buzzard]

Naturals are not a subset of the integers in Lean, they are two distinct types. If you want to make some things naturals and some things integers, then you are going learn how to move between these two types. An alternative is to just stick to integers everywhere.

[Kevin Buzzard]

Lean wants you to prove everything. Right now on line 42 you are making some construction which involves integers and you are claiming at the end that the result is a natural (the 0 on line 38 is a natural). To make this work you either have to insert a proof that this integer is always >= 0 and then cast it back to a natural, or you can ignore these issues and just take the norm of the integer (which is a natural, but of course now if you make a mistake in your code then changing a random sign here will make debugging even harder), or you can stop using naturals completely (my recommendation) and just work with integers, and then later on, if you need to, prove that one of those integers is always >= 0.

[Ocschwar]

I wound up sidestepping the issue for the purpose of this task by making depth an integer and enforcing it as a positive with comd.forward := max (0:ℤ )((position.depth p)+(position.aim p)*(instruction.length i) )

Thank you for the detailed explanation. The reason I'm fiddling with day 2 of Advent of Code on Dec 18th is that I want to understand this material and your explanations are a godsend.