Coq - Ошибка при устранении или

Question

я не знаю, почему, но в Coq, пытаясь доказать спецификацию программы я получаю сообщение об ошибке при попытке устранить ИЛИ гипотезу:

Error: Cannot find the elimination combinator or_rec, the elimination of the 
inductive definition Logic.or on sort Set is probably not allowed. 

Это теорема Я хочу, чтобы доказать:

Definition nat_div_mod : forall a b:nat, not(b=0) -> {qr:nat*nat | P a b qr}. 

Это цель и контекст, когда происходит ошибка:

a : nat 
b : nat 
H : b <> 0 
IHa : {qr : nat * nat | P a b qr} 
x : nat * nat 
H2 : P a b x 
H0 : snd x < b - 1 \/ snd x >= b - 1 
______________________________________ 
{qr : nat * nat | P (S a) b qr} 

до этого theore м, у меня есть это определение и эти импорт:

Definition P (a b:nat) (qr:nat*nat) : Prop := ... (* specification of div/mod *) 
Require Import Omega. 
Require Import Mult. 

я получаю предыдущую ошибку, когда я пытаюсь использовать эту тактику:

elim H0. 

Я действительно не знаю, что может быть причиной его.

Answer 1

Вы не можете проанализировать ситуацию на H0, потому что {qr : nat * nat | P (S a) b qr} является Set или Type. Только or_ind определен для or, поэтому вместо этого должно быть Prop. Если вы используете sum, у вас будет sum_ind, sum_rec и sum_rect.

(snd x < b - 1) + (snd x >= b - 1) 

Prop разработан таким образом, чтобы он был в соответствии с определенными аксиомами.