Default tactic argument?

Stream: lean4

[Avi Craimer]

When I'm writing a type that does a simple guard check using a proof of a proposition as an argument, is there a way to make the proof argument implicit and provide a default tactic.

Here is the example I'm working on.

inductive Context: List String -> Type where
| empty : Context []
| extend: (ctx: (Context names)) -> (name: String) ->
  (_: names.contains name = false) -> Context (name::names)

def cat := Context.extend Context.empty "cat" (by decide)

def catdog := Context.extend cat  "dog" (by decide)

def catdogcat := Context.extend catdog "cat" (by decide)
-- Can't add cat again, the tactic will fail.

This works fine, but I have to pass the argument (by decide) explicitly every time I use Context.extend. I tried making the third argument implicit like this:

inductive Context: List String -> Type where
| empty : Context []
| extend: (ctx: (Context names)) -> (name: String) ->
  {_: names.contains name = false} -> Context (name::names)

but I get the error:

don't know how to synthesize implicit argument
  @Context.extend [] Context.empty "cat" ?m.3624
context:
⊢ List.contains [] "cat" = false

Since this is always a decidable problem is there a way to give a hint to the compiler to use decide to synthesize the implicit argument?

[Marcus Rossel]

You can add a default argument for the proof parameter of the extend constructor:

inductive Context: List String -> Type where
| empty : Context []
| extend: (ctx: (Context names)) -> (name: String) ->
  (_: names.contains name = false := by decide) -> Context (name::names)

def cat := Context.extend Context.empty "cat"

def catdog := Context.extend cat  "dog"

def catdogcat := Context.extend catdog "cat"
-- Can't add cat again, the tactic will fail.

[Avi Craimer]

Thanks @Marcus Rossel I didn't know about default arguments in Lean!

[Avi Craimer]

As a follow up to this.

How do I define Repr. When I use the deriving Repr it fails, I guess because it can't print the proof term. How do I tell it to ignore the proof term when printing the Context term?

[Mario Carneiro]

right now you have to write Repr instances manually if deriving Repr fails

[Mario Carneiro]

instance (l) : Repr (Context l) := ...

[Avi Craimer]

--

[Avi Craimer]

I realized a simpler way to to the context would be like this:

abbrev  Context := { list: List String // list = list.eraseDups }

But then I don't know how to prove that if a list meets the property to be a context, then the tail of that list is also a Context.

i.e.,

def tail (ctx: Context): Context :=
  match ctx with
   |  ⟨ [], _ ⟩ =>  ⟨ [], by decide⟩
   |  ⟨ x::xs, p ⟩ => ⟨ xs, sorry ⟩

Clearly, I need to do something with p but I'm not sure what.

[Avi Craimer]

The other thing I'm struggling with is how to write a fromList function. I want to take a list, apply eraseDups and then produce a Context. It seems obvious, but I can figure out how to prove that list.eraseDups = list.eraseDups.eraseDups.

[Marcus Rossel]

This might not be what you want, but if you're ok with using Lean's Std library you can use docs#List.Nodup. Then you'll probably find the appropriate lemmas like docs#List.nodup_cons. And if you're ok with using Mathlib you could even go for docs#Finset.

[Avi Craimer]

@Marcus Rossel Thanks Marcus. As I'm still very new to using Lean, I haven't figured out how to import stuff from Mathlib. Do I need to create a project folder to do so? Up until now I've just been working in a single file using whatever is in Prelude.

[Ruben Van de Velde]

Yes, you need to create a project that depends on mathlib

[Mario Carneiro]

lake init myproj math