理由はわかりませんが、Coq でプログラム仕様を証明しようとすると、OR 仮説を排除しようとするとエラーが発生します。
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}
この定理の前に、次の定義とインポートがあります。
Definition P (a b:nat) (qr:nat*nat) : Prop := ... (* specification of div/mod *)
Require Import Omega.
Require Import Mult.
この戦術を使用しようとすると、前のエラーが発生します。
elim H0.
何が原因なのかよくわかりません。