Recomputable

[strake]

Given a decidable relation, we can rebuild a relevant proof given an irrelevant one. Please feel free to propose a better name if you have one! I wasn't sure what to call it.

[gallais]

Note that this type alias could readily be used in:

• Relation.Nullary's recompute

• Data.Rational.Properties' recomputeCP

I don't know what a good name for this principle would be though.

Edit: oh wait, no. It can only be used in Data.Rational.Properties. This is the
binary version of the unary principle we have in Relation.Nullary.

[strake]

@gallais We could use it in Data.Rational.Properties but i'm not sure how much we gain for a private lemma — Irrelevant′ (λ n d → Coprime n (suc d)) is not much shorter than ∀ {n d} → .(Coprime n (suc d)) → Coprime n (suc d).

[strake]

@gallais All done

[MatthewDaggitt]

Hmm for starters I agree with @strake that the current name isn't great. Perhaps something like Recomputable?

My second question is what's the use case for this? Are there instances of common non-decidable relations for which this holds? If not, and it's only useful in the two recomputable lemmas then perhaps it doesn't deserve it's own type?

[strake]

@MatthewDaggitt The obvious example to me is pointwise equality of functions given recomputable equality of the codomain:

module _ {a b} {A : Set a} {B : A → Set b} where
    _≃_ : Rel ((a : A) → B a) (a ⊔ b)
    f ≃ g = ∀ {a} → f a ≡ g a

    ≃-irrel′ : (∀ {a} → Irrelevant′ (_≡_ {_} {B a})) → Irrelevant′ _≃_
    ≃-irrel′ d x = d x

    ≃-dec : (∀ {a} → Decidable (_≡_ {_} {B a})) → Decidable _≃_
    ≃-dec d f g = {!!} -- I not believe it's provable.

Edit: This includes certain representations of ℝ, for example: ℕ → Bool (binary expansion, Stern-Brocot, whatever you like).

[strake]

And "Recomputable" is fine for me.

[strake]

@MatthewDaggitt Renamed as Recomputable.

[MatthewDaggitt]

Edit: This includes certain representations of ℝ, for example: ℕ → Bool (binary expansion, Stern-Brocot, whatever you like).

Thanks, that's a great example! Would you be able to add the Unary version as well for completeness? Also as it's a bit of an uncommon name I think the full name should probably be used, i.e. dec⟶recomputable rather than dec⟶recomput.

Once that's done, I'll merge it in.

[strake]

@MatthewDaggitt All done ☺