Automatically search for proofs

Stream: new members

[Felipe GS]

Are there ways to auto search proofs? I'm trying to make something similar to the code below , but I have no idea how to make these verbose ways to create a hetlist simpler to use.

inductive Under : List (Type u) → Type (u+1) where
  | nil  : x → Under (x :: xs)
  | cons : Under xs → Under (y :: xs)

-- Is there some way to write something like [2,"a"] and it automatically creates it
def hetList : List (Under [Int, String]) := [Under.nil 2, Under.cons (Under.nil "a")]

-- Or something to search by x \in xs
inductive HetList : List (Type u) → Type (u+1) where
  | nil  :  HetList b
  | cons :  x  → x ∈ xs →  HetList xs → HetList xs

-- It looks really bad :/
def httList : HetList [Int, String] :=
     HetList.cons 2   (List.Mem.head Int [String])
   $ HetList.cons "a" (List.Mem.tail Int $ List.Mem.head String [])
   $ HetList.nil

[Eric Wieser]

What would [1,2] mean for HetList [Int, Int]?

[Eric Wieser]

Because 1 could be either Under.nil 1 or Under.cons (Under.nil 1)

[Felipe GS]

So there's no way of making something like that because of the multiple ways to create a value for HetList [Int, Int]?

[Eric Wieser]

I mean, you could still make something like that, but the problem statement is ambiguous and lean can't read your mind about which interpretation you want

[Eric Wieser]

It could totally just always prefer the earlier items in the list in the cae of ambiguity

[Felipe GS]

So how can I get lean compiler to do that automatically?

[Eric Wieser]

I assume this is a Lean4 question? Does by decide work for the proof fields?