4
$\begingroup$

In Definitional Proof Irrelevance Without K, inductives in sProp need to satisfy three conditions to allow large elimination:

(1) Every non-forced argument must be in sProp.
(2) The return types of constructors must be pairwise orthogonal.
(3) Every recursive call must satisfy a syntactic guard condition

I have the following data definition in Agda (I have T, < defined elsewhere, but given as postulates here for a MWE):

{-# OPTIONS --prop #-}

postulate
  T : Set
  _<_ : T → T → Set

data Acc (x : T) : Prop where
  acc : (∀ y → y < x → Acc y) → Acc x

Now I'd like to throw caution to the wind and eliminate Acc to something in Set at the expense of, as I understand it, possible nonterminating type checking. Evidently right now that's not possible since Acc violates (3) (and this is explicitly stated as an example in the paper), yielding the type checking error:

Cannot split on datatype in Prop unless target is in Prop
when checking that the pattern acc p has type Acc x

Is there some way of only turning (3) off? Perhaps with something like {- NON_TERMINATING -}... somewhere? I'm confident I won't actually run into nontermination issues (I've previously proven the wellfoundedness of <, for one), and I'd like to type check the rest of my proofs without disregarding safety entirely.

EDIT: I'd be interested to know if it'd be possible to do the same in Coq as well, which currently gives me this error:

Fixpoints on proof irrelevant inductive types should produce proof irrelevant values.
$\endgroup$
0

2 Answers 2

4
$\begingroup$

AFAIK there is no way to turn it off. It is also worth pointing out that the cost is greater than you expected.

data A : Prop where
  a b : A

It is possible to prove eq : (B : Set)(f : A → B) → f a ≡ f b with refl. So if you were allowed to turn off the check, it does not leads to non-terminating type checking. Rather, it produces impossible cases and breaks subject reduction (i.e. if a term is well-typed, then after you perform evaluation of the term, it always remains well-typed).

In particular, in your case it immediately leads to a contradiction. You have a proof of False that is well-typed (of type Empty). But when you normalize it, the resulting term is no longer well-typed.

There are a few ways to solve this:

  • Use Set. Why did you use Prop in the first place?
  • Use Prop also for your target type. Why does it have to be in Set?
  • Postulate an elimination function using the postulate keyword. You should probably not expect any sort of computation, because that always breaks subject reduction.
$\endgroup$
6
  • $\begingroup$ What's the proof of Empty that I'd get if Acc in sProp were allowed to be eliminated? $\endgroup$
    – ionchy
    May 2 at 0:03
  • $\begingroup$ @ionchy Is it true that there are at most one element of each p < q? If so, simply prove that (or postulate that if you don't want to bother) and I think you wouldn't lose much using Set, you just have to insert transports along the way. If it is not the case, then my argument immediately applies. $\endgroup$
    – Trebor
    May 2 at 3:49
  • $\begingroup$ I am defining (well, postulating above) p < q in Set, it's Acc p rather that I'd like to put in sProp. The fact that any Acc p only has one proof is actually provable up to propositional equality if I postulate function extensionality, come to think of it. $\endgroup$
    – ionchy
    May 2 at 5:19
  • 1
    $\begingroup$ @ionchy Yes I misread. It's true that Acc is propositionally singletons. But if there are elements that are not equal on the nose (for instance, one function does a useless case analysis on the parameter, and another does not), it still breaks subject reduction. $\endgroup$
    – Trebor
    May 2 at 5:34
  • 2
    $\begingroup$ Having Acc in SProp (with its eliminator) shouldn't break consistency: you can embed that type theory in Extensional Type Theory (adding an equality reflection rule) which has models (at least in a metatheory that is strong enough, e.g., ZFC+enough inaccessible cardinals) $\endgroup$ May 2 at 9:02
3
$\begingroup$

In Coq, you can probably hack your way around by unsetting the guard condition and writing a fixpoint that is "semantically" guarded but not syntactically so. Something along the lines of what is below.

Inductive sAcc (A : Type) (R : A -> A -> Prop) (x : A) : SProp :=
| sAcc_intro : (forall y : A, R y x -> sAcc A R y) -> sAcc A R x.

#[bypass_check(guard)]
Definition sAcc_rect (A : Type) (R : A -> A -> Prop) (P : A -> Type)
  (f : forall x : A, (forall y : A, R y x -> sAcc A R y) -> (forall y : A, R y x -> P y) -> P x) :
  forall (x : A) (a : sAcc A R x), P x :=

  (fix F (u : unit) (x : A) (a : sAcc A R x) {struct u} : P x :=
    f x (match a with sAcc_intro _ _ _ a => a end)
      (fun y r => F tt y (match a with sAcc_intro _ _ _ k => k y r end))
  ) tt.

You have to be careful though, because this will explode as soon as you try to perform a weak head on this. So you'll have to work around unification and kernel type-checking by making some conversions explicit. Alternatively, you may try to guard the fixpoint by some dummy argument, e.g. by keeping the unit argument abstract.

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.