Fixing propositions

Stream: new members

[Pedro Minicz]

While trying to understand roption I came up with the following:

import control.fix

variables {α : Type*} (F : (α → Prop) → α → Prop)

def aux (f : α → roption unit) (a : α) : roption unit :=
⟨F (λ a, (f a).dom) a, λ _, ()⟩

def fix (a : α) : Prop :=
(roption.fix (aux F) a).dom

lemma aux_id_eq_id : @aux α id = id :=
by { ext f a ⟨⟩, simp [aux, has_mem.mem, roption.mem] }

example (a : α) : ¬fix id a :=
sorry

What is fix id a? I strongly believe it is false (intuition!), but how do I show that to Lean?

[Pedro Minicz]

Also, fix F a where F : (α → Prop) → α → Prop and a : α is not decidable in general. What sort of predicate over F would it be necessary to show that it is?

[Pedro Minicz]

(It feels really weird to write fix id in Lean, where fix has some resemblance to Haskell's fix, since fix id is an infinite loop! I strongly believe this translates into an undecidable proposition here.)

[Pedro Minicz]

Here we go.

example (a : α) : ¬fix id a :=
begin
  rintro ⟨⟨i, h₁⟩, h₂⟩,
  induction i with i ih,
  { exact h₁ },
  { exact ih h₁ h₂ }
end

[Pedro Minicz]

I am a bit bewildered by this proof. fix id a implies there is a natural number smaller than any natural number or larger than any natural number? (Does this question even make sense? I find it hard to describe what I am thinking.) Also, how roption.fix.approx works?

[Kenny Lau]

Could you explain what fix does?

[Pedro Minicz]

To be honest, I am not really sure, since I don't understand roption.fix. But I am going to give a (hopefully) educated guess.

roption is the following type:

/-- `roption α` is the type of "partial values" of type `α`. It
  is similar to `option α` except the domain condition can be an
  arbitrary proposition, not necessarily decidable. -/
structure {u} roption (α : Type u) : Type u :=
(dom : Prop)
(get : dom → α)

Note that roption unit is pretty much Prop. Also note that roption is a kind of continuation. fix F a return a proposition which is built recursively. This proposition may be is fully recursive (not "terminating" recursive, as functions in Lean). As such, it may not be decidable. roption acting like a continuation makes its construction "lazy" is some sense.

F : (α → Prop) → α → Prop can decide whether to or not to call its first argument. Therefore, it can branch depending on α. So the decidability fix F a (should) depend on F only.

[Pedro Minicz]

variables (f : (Π a, roption $ β a) → (Π a, roption $ β a))

/-- A series of successive, finite approximation of the fixed point of `f`, defined by
`approx f n = f^[n] ⊥`. The limit of this chain is the fixed point of `f`. -/
def fix.approx : stream $ Π a, roption $ β a
| 0 := ⊥
| (nat.succ i) := f (fix.approx i)

/-- The least fixed point of `f`.

If `f` is a continuous function (according to complete partial orders),
it satisfies the equations:

  1. `fix f = f (fix f)`          (is a fixed point)
  2. `∀ X, f X ≤ X → fix f ≤ X`   (least fixed point)
-/
protected def fix (x : α) : roption $ β x :=
roption.assert (∃ i, (fix.approx f i x).dom) $ λ h,
well_founded.fix.{1} (nat.upto.wf h) (fix_aux f) nat.upto.zero x

roption.fix.approx recurses a finite amount of times before returning an empty roption (e.i. a continuation which cannot be called; in our case just false). To call the roption continuation you need to prove that f returns after iterating a finite amount of times, that is, ∃ i, (fix.approx f i x).dom.

[Pedro Minicz]

I wonder how to get fix F = F (fix F) (in the cases where it is doable).

set_option pp.proofs true

example (hF : Π p a, decidable (F p a)) (a : α) : decidable (fix F a) :=
begin
  have := hF (fix F) a,
  unfold fix roption.fix roption.assert,
  simp,
  sorry
end

[Pedro Minicz]

"Beta reduced" fix.

import data.nat.upto

variables {α : Type} (f : (α → Prop) → α → Prop)

/-- A series of successive, finite approximation of the fixed point of `f`,
defined by `approx f n = f^[n] (λ _, false)`. The limit of this chain is the
fixed point of `f`. -/
def fix.approx : ℕ → α → Prop
| 0       := λ _, false
| (i + 1) := f (fix.approx i)

/-- Loop body for finding the fixed point of `f`. -/
def fix_aux {p : ℕ → Prop} (i : nat.upto p)
  (g : Π j : nat.upto p, i < j → α → Prop) : α → Prop :=
f $ λ a : α, ∃ h, g (i.succ h) (nat.lt_succ_self i) a

/-- The least fixed point of `f`.

If `f` is a continuous function (according to complete partial orders),
it satisfies the equations:

  1. `fix f = f (fix f)`          (is a fixed point)
  2. `∀ p, f p ≤ p → fix f ≤ p`   (least fixed point)
-/
def fix (a : α) : Prop :=
∃ h : ∃ i, fix.approx f i a,
  well_founded.fix (nat.upto.wf h) (fix_aux f) nat.upto.zero a

#print axioms nat.upto.wf
#print axioms nat.upto.succ

nat.upto.wf and nat.upto.succ are the culprits why fix uses classical.choice. I believe fix f is always computable (although the Prop it returns might not).

[Mario Carneiro]

In general, the domain of an roption is not decidable - in fact that's the whole point; an roption with decidable domain is equivalent to an option A

[Mario Carneiro]

but it's also not that useful to have decidability for the domain of a particular roption. Normally you would instead just prove it is true or false (depending on the situation)

[Mario Carneiro]

I find the simpler version pfun.fix easier to think about. This has the type (A -> roption (A + B)) -> A -> roption B, and the idea is that starting from an initial value A, you call the provided function repeatedly until you get a B. If the function never returns a B then the roption is empty

[Mario Carneiro]

You can define this without any choice principles; the domain of the roption is the proposition "there exists a finite sequence of calls f a0 = some (inl a1), f a1 = some (inl a2), ..., f an = some (inr b)", and under that assumption, the b that is obtained is uniquely defined

[Mario Carneiro]

This proposition is clearly not decidable in general - it is equivalent to the halting problem - but it is maximal in the sense that if the function terminates then pfun.fix will pick out the right answer, which makes it very useful to specify values that have not yet been shown to exist

[Mario Carneiro]

roption.fix adds some classical logic in order to make it total, but the classical logic is all contained in the domain proposition so it's still computable (because this only concerns the function part, which is still uniquely defined)