Zulip Chat Archive

Stream: maths

Topic: making mynat an add_comm_monoid


view this post on Zulip Kevin Buzzard (Jul 02 2019 at 23:21):

I was trying to prove that a home-rolled nat was an add_comm_monoid in a way which was maximally mathematician-friendly, e.g. no leakage of le or zero: see gist.

My understanding of how Lean works is that I am supposed to come up with a canonical representative for things like mynat.zero -- I choose 0, and similarly I choose 1 for one. That's right, right?

On line 56 I have a zero which is something I never really wanted to see again. Is there a more high-powered tactic which will preserve my choice for 0 as the "canonical representative" of mynat.zero?

Is there a tactic that makes that instance on line 77 by just matching on names?

Finally lines 142 and 146 -- what is the incantation which makes these? I am so bad at making structures. Let's say that you must make an instance of add_semigroup mynat before you make the instance of add_comm_semigroup mynat.

view this post on Zulip Keeley Hoek (Jul 03 2019 at 04:49):

Kevin I think your by common_sense actually is a pretty easily makable tactic

view this post on Zulip Keeley Hoek (Jul 03 2019 at 04:49):

I'll give it a go

view this post on Zulip Keeley Hoek (Jul 03 2019 at 05:07):

...

end mynat

namespace tactic.interactive
open tactic

meta def replace_special_names : name  name
| `add := `has_add.add
| n := n

meta def common_sense : tactic unit :=
do t  target,
   env  get_env,
   match t with
   | expr.app (expr.const sn _) e :=
    match env.structure_fields sn with
    | some l :=
    do n :: _  tactic.open_namespaces,
       let lf := l.map replace_special_names,
       v  lf.mmap resolve_name,
       let s : structure_instance_info := {
           struct := some sn,
           field_names := l,
           field_values := v,
       },
       e  to_expr $ pexpr.mk_structure_instance s,
       tactic.exact e
    | none := fail "goal not a structure"
    end
   | _ := fail "unsupported goal"
   end

end tactic.interactive

namespace mynat

instance : add_monoid mynat := by common_sense

...

view this post on Zulip Kevin Buzzard (Jul 03 2019 at 07:00):

It works! Thanks! I hate making structures. I will use it forever.

view this post on Zulip Kevin Buzzard (Jul 03 2019 at 07:08):

Oh this is great. I have no clue how you're supposed to prove that mynat is a comm_semiring. You seem to have to perform the incantations all in exactly the right order in the official way to do it. This way I can just not even care. I went to the end of my multiplication file and typed instance : comm_semiring mynat := by common_sense and it just gave me a list of the fields for which it has failed and what the error messages were for each. I can then just make them at the end of my multiplication file as part of an api. This is brilliant.

It's sort-of an idiot-proof structure maker.

view this post on Zulip Scott Morrison (Jul 03 2019 at 10:21):

Can we have this in mathlib? Maybe called structure_helper?

view this post on Zulip Patrick Massot (Jul 03 2019 at 11:34):

Kevin, could you post an updated gist using this tactic? It would make this conversation easier to understand

view this post on Zulip Kevin Buzzard (Jul 03 2019 at 13:25):

Structure tactic

add_comm_monoid nat

view this post on Zulip Patrick Massot (Jul 03 2019 at 13:49):

Nice! I hope mathlib's naming convention won't interfere with merging this useful tactic

view this post on Zulip Kevin Buzzard (Jul 03 2019 at 14:26):

@Keeley Hoek

I can't make preorders because they have this weird lt_iff_not_le field.

set_option auto_param.check_exists false
class preorder (α : Type u) extends has_le α, has_lt α :=
(le_refl :  a : α, a  a)
(le_trans :  a b c : α, a  b  b  c  a  c)
(lt := λ a b, a  b  ¬ b  a)
(lt_iff_le_not_le :  a b : α, a < b  (a  b  ¬ b  a) . order_laws_tac)

I just want to not define lt or lt_iff_le_not_le

-- import the tactic
inductive mynat : Type

namespace mynat

def le : mynat  mynat  Prop := sorry
instance : has_le mynat := le
def le_refl :  a : mynat, a  a := sorry
-- I think a,b,c should be implicit but Lean doesn't
def le_trans :  a b c : mynat, a  b  b  c  a  c := sorry

--instance : preorder mynat := by i_checked_all_teh_axioms -- fails
-- unknown identifier 'lt'

def lt : mynat  mynat  Prop :=  λ a b, a  b  ¬ b  a

-- instance : preorder mynat := by i_checked_all_teh_axioms -- fails
/-
type mismatch at field 'lt_iff_le_not_le'
  lt_iff_le_not_le
has type
  ?m_3 < ?m_4 ↔ ?m_3 ≤ ?m_4 ∧ ¬?m_4 ≤ ?m_3
but is expected to have type
  auto_param (∀ (a b : mynat), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous)
-/

end mynat
/-
class preorder (α : Type u) extends has_le α, has_lt α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b, a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)
-/

view this post on Zulip Scott Morrison (Jul 03 2019 at 14:30):

Ah, we'll have to add something that checks if a field is wrapped with auto_param, and then tries running the embedded tactic.

view this post on Zulip Mario Carneiro (Jul 03 2019 at 14:31):

or opt_param in the case of lt

view this post on Zulip Andrew Ashworth (Jul 03 2019 at 14:47):

hmm, wasn't there a hole tactic that did this as well that I saw posted awhile back? I may be misremembering

view this post on Zulip Patrick Massot (Jul 03 2019 at 14:48):

Do you mean https://github.com/leanprover-community/mathlib/blob/d001abfd48d64ac27310590458132009f47c852d/src/tactic/core.lean#L718? It's slightly different

view this post on Zulip Andrew Ashworth (Jul 03 2019 at 14:50):

ah, I think that is what I was thinking of

view this post on Zulip Kevin Buzzard (Jul 03 2019 at 14:59):

I just want to not even bother defining lt and lt_iff_le_not_le here

view this post on Zulip Scott Morrison (Jul 03 2019 at 15:11):

Yes, that's what we're proposing. Keeley's tactic should be able to identify opt_param or auto_param fields, and handle them automatically.

view this post on Zulip Keeley Hoek (Jul 03 2019 at 17:05):

I'm glad it helped! Yes this should be easy to fix...

view this post on Zulip Keeley Hoek (Jul 03 2019 at 17:10):

Oh hmm turns out it's a bit yuck...

view this post on Zulip Kevin Buzzard (Jul 03 2019 at 17:11):

instance : canonically_ordered_comm_semiring mynat :=
{ add := (+),
  add_assoc := add_assoc,
  zero := 0,
  zero_add := zero_add,
  add_zero := add_zero,
  add_comm := add_comm,
  le := (),
  le_refl := le_refl,
  le_trans := le_trans,
  le_antisymm := λ a b, le_antisymm,
  add_le_add_left := add_le_add_left,
  lt_of_add_lt_add_left := lt_if_add_lt_add_left,
  bot := _,
  bot_le := bot_le,
  le_iff_exists_add := le_iff_exists_add,
  mul := (*),
  mul_assoc := mul_assoc,
  one := 1,
  one_mul := one_mul,
  mul_one := mul_one,
  left_distrib := left_distrib,
  right_distrib := right_distrib,
  zero_mul := zero_mul,
  mul_zero := _,
  mul_comm := _,
  zero_ne_one := _,
  mul_eq_zero_iff := _ }

Also yuck.

view this post on Zulip Keeley Hoek (Jul 03 2019 at 17:37):

ha! its literally 3am where I am at the moment so I'm going to throw in the towel until morning---but just one last sorried function needs filling in:

view this post on Zulip Keeley Hoek (Jul 03 2019 at 17:37):

namespace tactic.interactive
open tactic

meta def replace_special_names : name  name
| `add := `has_add.add
| n := n

meta def get_type_of_nth_arg_core :   expr  expr
| _ _ := sorry

meta def get_type_of_nth_arg (n : name) (k : ) : tactic expr :=
get_type_of_nth_arg_core k <$> (resolve_name n >>= to_expr >>= infer_type)

meta def run_tac (n : expr) : tactic unit :=
do n  eval_expr name n,
   e  resolve_name n >>= to_expr,
   tac  eval_expr (tactic unit) e,
   tac

meta def resolve_name_or_use_autoparam (sn : name) (n :  × name) : tactic (name × pexpr) :=
do pe  resolve_name (replace_special_names n.2) <|>
        do { t : expr  get_type_of_nth_arg (sn ++ `mk) n.1,
             match t with
             | `(auto_param %%t %%tac) :=
               lock_tactic_state $ do
                 m  mk_meta_var t,
                 set_goals [m],
                 run_tac tac,
                 to_pexpr <$> instantiate_mvars m
             | _ := failed
             end
           },
   return (n.2, pe)

meta def i_checked_all_teh_axioms : tactic unit :=
do t  target,
   env  get_env,
   match t with
   | expr.app (expr.const sn _) e :=
    tactic.trace (env.structure_fields sn) >>
    match env.structure_fields sn with
    | some l :=
    do n :: _  tactic.open_namespaces,
       let l := (list.range l.length).zip l,
       v  l.mfilter_map $ resolve_name_or_use_autoparam sn,
       tactic.trace v,
       let s : structure_instance_info := {
           struct := some sn,
           field_names := v.map prod.fst,
           field_values := v.map prod.snd,
       },
       tactic.trace v,
       e  to_expr $ pexpr.mk_structure_instance s,
       tactic.exact e
    | none := fail "goal not a structure"
    end
   | _ := fail "unsupported goal"
end

end tactic.interactive

view this post on Zulip Keeley Hoek (Jul 03 2019 at 17:38):

haha funnily enough run_tac is equivalent to the ridiculous composite

meta def run_tac' (n : expr) : tactic unit :=
do tac  eval_expr name n >>= resolve_name >>= to_expr >>= eval_expr (tactic unit),
   tac

view this post on Zulip Kevin Buzzard (Jul 03 2019 at 17:50):

instance : canonically_ordered_comm_semiring mynat :=
{ add := (+),
  add_assoc := add_assoc,
  zero := 0,
  zero_add := zero_add,
  add_zero := add_zero,
  add_comm := add_comm,
  le := (),
  le_refl := le_refl,
  le_trans := le_trans,
  le_antisymm := λ a b, le_antisymm,
  add_le_add_left := add_le_add_left,
  lt_of_add_lt_add_left := lt_if_add_lt_add_left,
  bot := ,
  bot_le := bot_le,
  le_iff_exists_add := le_iff_exists_add,
  mul := (*),
  mul_assoc := mul_assoc,
  one := 1,
  one_mul := one_mul,
  mul_one := mul_one,
  left_distrib := left_distrib,
  right_distrib := right_distrib,
  zero_mul := zero_mul,
  mul_zero := mul_zero,
  mul_comm := mul_comm,
  zero_ne_one := zero_ne_one,
  mul_eq_zero_iff := mul_eq_zero_iff }

I finished my proof.

view this post on Zulip Kenny Lau (Jul 03 2019 at 17:54):

how about decidable le?

view this post on Zulip Kevin Buzzard (Jul 03 2019 at 17:55):

Oh that's not maths, that's not in this game

view this post on Zulip Kevin Buzzard (Jul 03 2019 at 17:55):

That is generated without telling the user

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 07:45):

how about decidable le?

decidable le uses recursion. I am trying to box off what is done by recursion, because mathematicians put it in a different box to induction.

Example: one could present the natural numbers mynat as having two constants mynat.zero and mynat.succ, two axioms mynat.zero_ne_succ and mynat.succ_inj, and one key fact: you can use the induction n tactic if you have n : mynat. The two axioms are proved by Lean using recursion via nat.rec; succ_inj can be proved easily using the completely artificial function pred which no mathematician has ever seen or uses (because it allows 0 as an input and gives the wrong answer), and zero_ne_succ can be proved by defining a function which sends 0 to tt and succ n to ff, again a function which can be defined by recursion but is of no use to us in practice.

If you present nat this way and present addition similarly (mynat.add is a constant, we will always use the + notation, add_zero and add_succ are axioms, don't worry about how it was defined) then one can "prove" things like the "theorem" add_monoid mynat (because now it is a theorem -- all the data has been given to you and there's only a theorem left) purely within tactic mode, by supplying tactic proofs of each of the fields in whatever order you like.

I am looking at what happens to nat if you try and isolate all the computational content and "proofs and data constructed via recursion" and just give the user an inductive principle which can only be used to construct proofs. One way of looking at it is you could say that I was trying to isolate "the bit which mathematicians like best".

view this post on Zulip Keeley Hoek (Jul 04 2019 at 10:14):

Update: it almost works, but its hard to tell when a structure has optional parameters (the "auto-param" kind is fine). It turns out that the generated constructors don't have the opt_param part...

view this post on Zulip Keeley Hoek (Jul 04 2019 at 10:16):

But otherwise it's a lot more robust than before now

view this post on Zulip Keeley Hoek (Jul 04 2019 at 10:23):

Okay I found a tricksy way (not intended, but I don't think there is an API for this...)

view this post on Zulip Keeley Hoek (Jul 04 2019 at 10:48):

Ok its even tricker than I thought, extra idea...

view this post on Zulip Keeley Hoek (Jul 04 2019 at 11:13):

Yeah ok I'm really struggling. There is a lot of code now, and by some tricks I can find out which fields have optional/default values, but I can't find a way to determine what the values actually are. Secretly lean knows, but I think it might not be exposed. Does anyone know of a way to find the default value of a field declared opt_param?

view this post on Zulip Keeley Hoek (Jul 04 2019 at 11:14):

(Sounds like this might be a job for lean 3.5.0, just need to add a function)

view this post on Zulip Keeley Hoek (Jul 04 2019 at 11:17):

Here is the current state: https://gist.github.com/khoek/b820b0b242909a22bfd3b16a046eb9de
It does everything you want Kevin except for the lt problem.

view this post on Zulip Mario Carneiro (Jul 04 2019 at 11:23):

try_apply_opt_auto_param_for_apply might help as a template. It uses

when cfg.opt_param (try apply_opt_param) >>
when cfg.auto_param (try apply_auto_param)

view this post on Zulip Mario Carneiro (Jul 04 2019 at 11:24):

which are themselves implemented in lean in the obvious way

view this post on Zulip Mario Carneiro (Jul 04 2019 at 11:25):

but they are expecting the opt/auto_param to be the main goal, not sure if that's true in your case

view this post on Zulip Keeley Hoek (Jul 04 2019 at 13:54):

I can do the handling of those cases just fine (and that code is in the gist), the problem is that there is no way at all I can find to programmically get the opt_param blah associated to an optional field of a structure.

view this post on Zulip Keeley Hoek (Jul 04 2019 at 13:55):

If you make an example structure which has an optional and auto param for comparison, the autogenerated .mk retains the autoparam but drops the optional

view this post on Zulip Mario Carneiro (Jul 04 2019 at 13:55):

An optional field has the type opt_param type default_value

view this post on Zulip Keeley Hoek (Jul 04 2019 at 13:56):

Sure, but this information is not exposed by lean

view this post on Zulip Mario Carneiro (Jul 04 2019 at 13:56):

it's literally in the expr

view this post on Zulip Keeley Hoek (Jul 04 2019 at 13:56):

The expr for what?

view this post on Zulip Mario Carneiro (Jul 04 2019 at 13:56):

the type of the projection

view this post on Zulip Keeley Hoek (Jul 04 2019 at 13:56):

oooooooh!

view this post on Zulip Keeley Hoek (Jul 04 2019 at 13:57):

Hang on

view this post on Zulip Keeley Hoek (Jul 04 2019 at 13:57):

run_cmd (do
  tactic.mk_const `preorder.lt >>= tactic.infer_type >>= pp >>= tactic.trace
)

view this post on Zulip Keeley Hoek (Jul 04 2019 at 13:58):

I don't see any reference to the opt_param

view this post on Zulip Keeley Hoek (Jul 04 2019 at 13:58):

The constructor preorder.mk is the same; auto_param fields are replicated, the optional ones are dropped

view this post on Zulip Mario Carneiro (Jul 04 2019 at 14:11):

Oh, that's weird... I found a strange parsing issue while investigating this too

structure preorder1 (α : Type) [has_le α] :=
(le_refl :  a : α, a  a)
(le_trans :  a b c : α, a  b  b  c  a  c)
(lt := λ a b : α, a  b  ¬ b  a)
(lt_iff_le_not_le :  a b : α, lt a b  (a  b  ¬ b  a) := λ _ _, iff.rfl)

structure preorder2 (α : Type) [has_le α] :=
(le_refl :  a : α, a  a)
(le_trans :  a b c : α, a  b  b  c  a  c)
(lt : α  α  Prop := λ a b : α, a  b  ¬ b  a)
(lt_iff_le_not_le :  a b : α, lt a b  (a  b  ¬ b  a) . order_laws_tac)

The type of lt_iff_le_not_le is different in the two cases. preorder2 is the right one. preorder1.lt_iff_le_not_le is trivial as evidenced by the rfl proof. @Sebastian Ullrich Are you aware of this? It looks like that thing you pointed out a while back where structures could define lets and notation and other crazy things. Somehow lt is treated as a notation for the purposes of lt_iff_le_not_le, but it is also an actual field...?

view this post on Zulip Keeley Hoek (Jul 04 2019 at 14:12):

:0

view this post on Zulip Mario Carneiro (Jul 04 2019 at 14:12):

The other weird thing about this is that lt is already defined in the case of preorder, in has_lt, and it's getting "redefined" with a new defeq type in preorder

view this post on Zulip Mario Carneiro (Jul 04 2019 at 14:13):

I can already predict that the lean C++ code to make sense of all this is a rats nest

view this post on Zulip Sebastian Ullrich (Jul 04 2019 at 14:16):

Looks like a straight bug

view this post on Zulip Patrick Massot (Jul 04 2019 at 14:17):

Now is the time were Sebastian will paste that url to the commit which fixed that bug in Lean 4 months ago

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 14:43):

I can make a preorder by just ignoring the lt and lt_iff_whatever fields completely. It's not possible to emulate that behaviour with a tactic?

view this post on Zulip Keeley Hoek (Jul 04 2019 at 14:55):

It appears that lean does not provide a way for lean to access the pre-set optional values of structures, eg. lt in this case.
I think I make it work but it'll be a little bit less robust than I had hoped

view this post on Zulip Keeley Hoek (Jul 04 2019 at 16:17):

@Kevin Buzzard Here is a link to something that works, at least on the two add_monoid and preorder examples I've seen! https://gist.github.com/khoek/cfb72fe41b0725269a14bf9196bb9c73

view this post on Zulip Keeley Hoek (Jul 04 2019 at 16:29):

Are you able to make a canonically_ordered_comm_semiring using it?

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:34):

I'm now seeing all sorts of errors like

type mismatch at field 'lt_of_add_lt_add_left'
  lt_of_add_lt_add_left
has type
  ?m_3 + ?m_4 < ?m_3 + ?m_5 → ?m_4 < ?m_5
but is expected to have type
  ∀ (a b c : mynat), a + b < a + c → b < c

but this is not your fault -- I have defined lt_of_add_lt_add_left with the inputs implicit but apparently Lean wants them explicit. Nearly there now, just fixing all of them.

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:36):

instance : canonically_ordered_comm_semiring mynat := by structure_helper -- works!

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:37):

How do I get a complete list of all the typeclasses X such that type class inference can find a term of type X nat ?

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:40):

But it works :-) Many thanks Keeley!

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:46):

Ultimately I would rather lt_of_add_lt_add_left : ∀ {a b c : mynat}, a + b < a + c → b < c := ... because I believe that this is the idiomatic way to define this function, with a, b, c implicit. It stops the tactic working through. We can put that down to "further work if someone can be bothered".

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:50):

@Mario Carneiro you were talking about a bug in Lean. Can this bug be easily fixed in 3.5.1? Would a consequence be that a whole bunch of _'s would need to be removed from mathlib? I feel like the definition of canonically_ordered_comm_semiring.lt_of_add_lt_add_left is "wrong".

canonically_ordered_comm_semiring.lt_of_add_lt_add_left : ∀ (a b c : ?M_1), a + b < a + c → b < c

I want to write some sort of front end for Lean where the user just has to type in simple proofs in tactic mode and that's all they can do. For this project, I don't care about mathlib and I don't care if I'm running a non-standard Lean. On the other hand if people change the behaviour of core tactics like induction then it will break everything I guess.

view this post on Zulip Mario Carneiro (Jul 04 2019 at 16:51):

You should just be using lt_of_add_lt_add_left

view this post on Zulip Mario Carneiro (Jul 04 2019 at 16:51):

which has the right binders

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:52):

ooh. ordered_cancel_comm_monoid

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:53):

I love that there are just a gazillion really stupid-in-my-eyes classes which are just out there and I don't know the names of any of them.

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:53):

I don't want to use it, I want the user to prove it.

view this post on Zulip Mario Carneiro (Jul 04 2019 at 16:54):

There is a tactic that does the restating automatically

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:55):

Yeah but I don't want to restate it, I want the user to prove it.

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:55):

We're building nat from scratch.

view this post on Zulip Mario Carneiro (Jul 04 2019 at 16:55):

The binders don't matter if you are proving it

view this post on Zulip Mario Carneiro (Jul 04 2019 at 16:55):

it's lambda regardless

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:55):

I know, I just feel like I'm lying to the user.

view this post on Zulip Mario Carneiro (Jul 04 2019 at 16:56):

In fact, it's usually better for the axiom to have all explicit or semi implicit binders when proving it

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:58):

@Keeley Hoek I would like an over-ride. I'd like to define mynat.lt_of_add_lt_add_left with semi-implicit or implicit binders, and then define mynat.lt_of_add_le_add_left' to be the thing with the stupid binders and then tell your tactic to use the stupid version with the ' just for that field only.

view this post on Zulip Mario Carneiro (Jul 04 2019 at 16:58):

For instance, you might have an assumption that says ∀ (a b c : A), a + b < a + c → b < c and you want to pass it in; if the assumption is implicit then the arguments will get auto applied and it won't fit

view this post on Zulip Mario Carneiro (Jul 04 2019 at 16:58):

I would assume that for Keeley's tactic you can define the binders however you like

view this post on Zulip Keeley Hoek (Jul 04 2019 at 17:01):

Unfortunately Mario it seems that the structure-builder notation refuses to accept specifying a field with different binders =/

view this post on Zulip Keeley Hoek (Jul 04 2019 at 17:01):

Perhaps another bug?

view this post on Zulip Keeley Hoek (Jul 04 2019 at 17:02):

MWE:

structure thingo :=
(func : Π (a : ), )

-- works
def foo : thingo := {func := λ {a : }, a + 1}

def concrete {a : } :  := a + 1
-- doesn't
def bar : thingo := {func := concrete}

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 17:04):

canonically_ordered_comm_semiring
  canonically_ordered_monoid,
    ordered_comm_monoid
      add_comm_monoid
      partial_order
    lattice.order_bot
      partial_order
  comm_semiring
  zero_ne_one_class

Generated by hand -- each thing extends the things one level of indentation below it.

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 17:06):

That's funny because you would imagine that lam a, f is syntactically equal to lam {a}, f

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 17:07):

structure thingo :=
(func : Π (a : ), )

-- works
def foo : thingo := {func := λ {a : }, a + 1}

-- also works!
def concrete {{a : }} :  := a + 1

def bar : thingo := {func := concrete}

view this post on Zulip Mario Carneiro (Jul 04 2019 at 17:27):

that's not a bug, that's by design

view this post on Zulip Mario Carneiro (Jul 04 2019 at 17:27):

and that's also why I said semi-implicit is a good choice here

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 17:29):

Is there a "correct" decision for the variables in lt_of_add_le_add_left ? Or do you sometimes need one thing and sometimes another?

view this post on Zulip Mario Carneiro (Jul 04 2019 at 17:35):

It might work to use apply to figure out the right number of arguments

view this post on Zulip Keeley Hoek (Jul 05 2019 at 14:54):

ooh, well my tactic could count the number of expected explicit arguments and then instead of fn := fn not compiling fn := \lambda a b, @fn _ a b would compile. Would that have defeq problems?

view this post on Zulip Mario Carneiro (Jul 05 2019 at 14:55):

no

view this post on Zulip Mario Carneiro (Jul 05 2019 at 14:56):

In principle this is what apply is supposed to do, but it may not work for you

view this post on Zulip Keeley Hoek (Jul 05 2019 at 14:57):

Yes, due to the aforementioned opt_param problems the only way I can get those fields filled is using a structure_instance_info, which needs explicit pexprs to be provided.

view this post on Zulip Keeley Hoek (Jul 05 2019 at 14:58):

Also, is your "no" an answer to my question, or "no that won't work"?

view this post on Zulip Mario Carneiro (Jul 05 2019 at 14:58):

no defeq problems

view this post on Zulip Mario Carneiro (Jul 05 2019 at 14:58):

You can elaborate an expr using apply and then quote it to turn it into a pexpr

view this post on Zulip Keeley Hoek (Jul 05 2019 at 15:26):

Oh ok, I see what you are saying. I tried something like this for a bit but there were problems I think with the inter-dependence of the fields and things like le not being decided when le_refl was being decided using an apply. I guess you could build everything consistently so that all the fields of the structure had metavariables in their type in common when they correspond to the same thing? But this seems like some work

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 15:29):

I am using Mario's approach of {{ }} when necessary


Last updated: May 12 2021 at 07:17 UTC