Total Idris newbie question, sorry.I've been taught in school there are natural numbers (N) and natural numbers with zero (N0).In Idris, there is data type Nat which corresponds to N0 by definition.What would change if there will be Nat defined as follows:data Nat = One | S Natdata Nat0 = Zero | NatI guess it's easier now, but is it mainly compiler implementation issue or formal one?There must be cases where 0 doesn't make sense and I guess these are more complicated to define correctly now.Or not?...Read more

I'm working through chapter 7 – Inductive Types of "Theorem Proving in Lean".I'd like to know how to write the definition of dependent non-dependent product in a more expanded or "primitive" form.It looks like the definition given in the tutorial automatically infers some detail:inductive prod1 (α : Type u) (β : Type v)| mk : α → β → prod1Some experimentation allows to fill in the detail inductive prod2 (α : Type u) (β : Type v) : Type (max u v)| mk : α → β → prod2However giving the definition in a fully expand form, using Pi types fails to typ...Read more

I'd like to do some work in topology using lean.As a good start, I wanted to prove a couple of simple lemmas about sets in lean.For exampledef inter_to_union (H : a ∈ set.inter A B) : a ∈ set.union A B := sorryor def set_deMorgan : a ∈ set.inter A B → a ∈ set.compl (set.union (set.compl A) (set.compl B)) :=sorryor, perhaps more interestinglydef set_deMorgan2 : set.inter A B = set.compl (set.union (set.compl A) (set.compl B)) :=sorryBut I can't find anywhere elimination rules for set.union or set.inter, so I just don't know how to work with t...Read more

I try using the syntax for inductive datatypes but it got an error message "mutually inductive types must compile to basic inductive type with dependent elimination".Below is an example of my attempt to define propositions even and odd on natural numbersmutual inductive even, oddwith even: ℕ → Prop| z: even 0| n: ∀ n, odd n → even (n + 1)with odd: ℕ → Prop| z: odd 1| n: ∀ n, even n → odd (n + 1)Also a related question: What is the syntax for defining mutually recursive functions? I can't seem to find it documented anywhere....Read more

Say I have a type:inductive is_sorted {α: Type} [decidable_linear_order α] : list α -> Prop| is_sorted_zero : is_sorted []| is_sorted_one : Π (x: α), is_sorted [x]| is_sorted_many : Π {x y: α} {ys: list α}, x < y -> is_sorted (y::ys) -> is_sorted (x::y::ys)And it's decidable:instance decidable_sorted {α: Type} [decidable_linear_order α] : ∀ (l : list α), decidable (is_sorted l)If I have a particular list:def l1: list ℕ := [2,3,4,5,16,66]Is it possible to prove that it's sorted at "compile time"; to produce an is_sorted l1 at the top...Read more

Lean comes with a decidable_linear_order typeclass containing useful lemmas about an ordering and its relation to equality, such as:lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < aThe equalities in these orderings are all expressed in terms of =:inductive eq {α : Sort u} (a : α) : α → Prop| refl : eq aI was wondering whether it would be possible to somehow extend this class (and its superclasses) to work with an arbitrary used defined equality relation R: α → α → Prop that was reflexive, symmetri...Read more

I'm trying to prove in Lean that if an item is less than the head of a sorted list, it's not a member of the list.theorem not_in_greater {α: Type} [d: decidable_linear_order α] {x h: α} (t: list α) (Hs: is_sorted (h::t)) (Hlt: x < h) : x ∉ (h::t) :=match t with | [] := not_eq_not_in (ne_of_lt Hlt) | (y::ys) := have x_neq_h: x ≠ h, from ne_of_lt Hlt, have sorted_tail: is_sorted (y::ys), from _After matching on t, the tail of the list, as (y::ys), I expected the assumption Hs: is_sorted (h::t) to be propagated, adding is_sorted (y...Read more

Are there any examples of Idris that might be used to study and perhaps apply it for general purpose/"real world" application?I am moderately proficient in Haskell, of which Idris seems to borrow significantly, and the official FAQ/documentation is rather nice but it would be very helpful to have some larger examples to explore. The goal is attempting to use Idris for practical software development. TIA....Read more

I'm facing a problem in Idris, where I want to create a type-level "check" based on a decidable property, where if the property holds I get the type I want, but if the property fails I get Unit (()), signaling that the program is in an inconsistent state (and should not compile if I decide to use it as my original type).Here's an example:TestType : {k : Nat} -> Nat -> Vect k Nat -> TypeTestType n ls with (isElem n ls) TestType n ls | Yes _ = Nat TestType n ls | No _ = ()mkTestTypeFromNat : (n : Nat) -> (ls : Vect k Nat) -> Elem...Read more

In Idris you can have complex computations in the types themselves, like a case block in this function:fun_1 : (n : Nat) -> case n of { Z => Bool; _ => Nat}fun_1 Z = Truefun_1 (S n) = S nBut how would you be able to fully evaluate such a result, given a n : Nat (which would evaluate into Bool or Nat)?For reference I have this function definition:fun_2 : (n : Nat) -> n = Z -> Boolfun_2 n nEqZ = ?fun_2_rhsHow could I implement this function using fun_1 so that it typechecks? I tried the following two approaches, which both gave an ...Read more

For my first formalization. I want to define polynomials in Lean. The first attempt is shown below:def polynomial (f : ℕ → ℤ ) (p: (∃m:ℕ , ∀ n : ℕ, implies (n≥m) (f n = (0:ℤ ) ) )):= fNow a want to test my definition using:def test : ℕ → ℤ | 0 := (2:ℤ )| 1 := (3:ℤ )| 2 := (4:ℤ )| _ := (0:ℤ )But I am having trouble constructing the proof term: def prf : (∃m:ℕ , ∀ n : ℕ, implies (n≥m ) (test n = (0:ℤ ) ) ):= exists.intro (3:ℕ ) ( assume n : ℕ, nat.rec_on (n:ℕ) () () )Also feedback on the definition itself is welcome....Read more

I'm learning the Lean proof assistant. An exercise in https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html is to define the predecessor function for the natural numbers. Can someone help me with that?...Read more

Given a proof of set inclusion and its converse I'd like to be able to show that two sets are equal.For example, I know how to prove the following statement, and its converse:open setuniverse uvariable elem_type : Type uvariable A : set elem_typevariable B : set elem_typedef set_deMorgan_incl : A ∩ B ⊆ set.compl ((set.compl A) ∪ (set.compl B)) := sorryGiven these two inclusion proofs, how do I prove set equality, i.e.def set_deMorgan_eq : A ∩ B = set.compl ((set.compl A) ∪ (set.compl B)) := sorry...Read more

I'm trying to understand inductive types from chapter 7 of "theorem proving in lean".I set myself a task of proving that successor of natural numbers has a substitution property over equality:inductive natural : Type| zero : natural| succ : natural -> naturallemma succ_over_equality (a b : natural) (H : a = b) : (natural.succ a) = (natural.succ b) := sorryAfter some guesswork and fairly exhaustive search I was able to satisfy the compiler with a couple of possibilities:lemma succ_over_equality (a b : natural) (H : a = b) : (natural.succ a)...Read more

I'm working my way through the chapter 4 of the lean tutorial.I'd like to be able to prove simple equalities, such as a = b → a + 1 = b + 1 without having to use the calc environment. In other words I'd like to explicitly construct the proof term of:example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := sorryMy best guess is that I need to use eq.subst and some relevant lemma about equality on natural numbers from the standard library, but I'm at loss. The closest lean example I can find is this:example (A : Type) (a b : A) (P : A → Prop) (H1 : a ...Read more