How do I translate Agda's "postulate" to Lean?

Stream: new members

[Eduardo Ochs]

Is there a way to translate Agda's "postulate" command to Lean?

As a curiosity/for the sake of completeness, here's what I would like to use it for. I am adding lots of snippets to my notes on Lean, and it would be nice to be able to generalize this test

#check do let a ← [1, 2] ; let b ← [a+1, a+2]; return (a,b)

to something like:

postulate (A : Type) (a1 a2 : A)
postulate (B : Type) (b1 b2 : B)
postulate (f1 f2 : A → B)
#check do let a ← [a1,a2] ; let b ← [b1,b2]; return (a,b)
#check do let a ← [a1,a2] ; let b ← [f1 a, f2 a]; return (a,b)

which means that a definition for "postulate" that is a quick hack using "sorry" would be perfectly fine...

[Damiano Testa]

Does your first code work for you?

[Damiano Testa]

Maybe, though, variable is what you are looking for?

[Eduardo Ochs]

The first - the one-liner - works. But try this:

variable (A : Type) (a1 a2 : A)
variable (B : Type) (b1 b2 : B)
variable (f1 f2 : A → B)

#check do let a ← [a1, a2]; let b ← [b1, b2]; return (a,b)
#check do let a ← [a1, a2]; let b ← [f1 a, f2 a]; return (a,b)

I got lots of "failed to synthesize instance" errors...

[Damiano Testa]

I get the same errors on the first as well...

[Joachim Breitner]

Agda's postulate corresponds to lean's axiom, I believe

[Eduardo Ochs]

GAAAAH! My fault!!! Try this:

instance : Monad List  where
  pure := List.pure
  bind := List.bind

#check do let a ← [1, 2] ; let b ← [a+1, a+2]; return (a,b)

variable (A : Type) (a1 a2 : A)
variable (B : Type) (b1 b2 : B)
variable (f1 f2 : A → B)

#check do let a ← [a1, a2]; let b ← [b1, b2]; return (a,b)
#check do let a ← [a1, a2]; let b ← [f1 a, f2 a]; return (a,b)

variable {A : Type} {a1 a2 : A}
variable {B : Type} {b1 b2 : B}
variable {f1 f2 : A → B}

#check do let a ← [a1, a2]; let b ← [b1, b2]; return (a,b)
#check do let a ← [a1, a2]; let b ← [f1 a, f2 a]; return (a,b)

It works. Sorry (and thanks)!