Zulip Chat Archive

Stream: general

Topic: equation compiler and dependent types


view this post on Zulip Patrick Massot (Dec 23 2018 at 16:45):

Is there any way to use the equation compiler with a dependent output? The following works (although I wish the proof part could be by linarith):

def euclid :   { n :  | 0 < n }   × 
| m n := if h : m < n then
           (0, m)
         else
           have (0 : ) < n, from n.property,
           have m - n < m, by apply nat.sub_lt ; linarith,
           let q, r := euclid (m-n) n in q+1, r

But now suppose I want the output type to be { p : ℕ × ℕ | m = n*p.1 + p.2 ∧ p.2 < n}. Is something like this possible? Of course here Lean complains it doesn't know who are m and n, which will appear only after matching. Of course I also wish I could write { (q, r) : ℕ × ℕ | m = n*q + r ∧ r < n} (or with angle brackets)instead of those ugly p.1 and p.2, but at least this is not blocking.

view this post on Zulip Patrick Massot (Dec 23 2018 at 16:58):

Sorry about this stupid question

view this post on Zulip Patrick Massot (Dec 23 2018 at 16:58):

I can use a Pi type instead

view this post on Zulip Patrick Massot (Dec 23 2018 at 17:07):

Note for next time I ask: one possible answer is

def euclid : Π (m : ) (n : { n :  // 0 < n }), {p :  ×  // m = n*p.1 + p.2  p.2 < n}
| m n := if h : m < n then
           (0, m), by simp *⟩
         else
           have (0 : ) < n, from n.property,
           have m - n < m, by apply nat.sub_lt ; linarith,
           let ⟨⟨q, r, H, H'⟩⟩ := euclid (m-n) n in
             (q+1, r),
              begin
                rw nat.sub_eq_iff_eq_add (le_of_not_lt h) at H,
                simp [H], ring,
               end, H'⟩⟩

Last updated: May 14 2021 at 13:24 UTC