Вычислить, если в решающей рек - PullRequest
Новая
       5

Вычислить, если в решающей рек

0 голосов
/ 07 июня 2018

Я хочу написать функцию, которая вычисляет количество истинных значений p 0 .. pt в функции nat-> prop. 

Section count_sc.

Variable p:nat->Prop.
Hypothesis p_dec:forall x:nat , {p x} + { ~ p x }.

Fixpoint count (x : nat) :=
    match x with
      | 0 => if p_dec(0) then 1 else 0
      | S y => if p_dec(x) then 1+count y else count y
    end. 

End count_sc.

Definition fret (x:nat) := False.

Check count.

Axiom fret_dec : forall x : nat , { fret x } + { ~ fret x }.


Theorem hello_decide : forall x : nat , count fret fret_dec x = 0.
Proof.
  intros.
  induction x.
  unfold count.
  replace (fret_dec 0) with false.
  
Qed.

Перед тактикой замены я должен доказать некоторую цель следующим образом:

(если fret_dec 0, то 1 еще 0) = 0

Доза Coq не рассчитывает автоматически значение if.и если я попытаюсь заменить fret_dec его значением, я получу эту ошибку:

Ошибка: термины не имеют конвертируемых типов.

Как я могу написать функцию подсчета, которую я могу развернуть ииспользовать это в теоремах?

1 Ответ

0 голосов
/ 07 июня 2018

Вы объявили fret_dec аксиомой.Но это означает, что у него нет определения или реализации другими словами.Таким образом, Coq не может вычислить с ним.

Вы все еще можете доказать свою теорему так, используя тактику destruct: 

Theorem hello_decide : forall x : nat , count fret fret_dec x = 0.
Proof.
  induction x as [| x IH].
  - unfold count. destruct (fret_dec 0) as [contra | _].
    + contradiction. 
    + reflexivity.
  - simpl. rewrite IH. destruct (fret_dec (S x)) as [contra | _].
    + contradiction.
    + reflexivity.
Qed.

Но, в этом случае это действительно легко обеспечитьтакая процедура принятия решения вместо того, чтобы постулировать это.И это сильно упрощает доказательство: 

Definition fret_dec' (x : nat) : { fret x } + { ~ fret x }.
Proof. right. intros contra. contradiction. Defined.

Theorem hello_decide' : forall x : nat , count fret fret_dec' x = 0.
Proof.
  induction x as [|x IH]; simpl.
  - reflexivity. 
  - exact IH.
Qed.
...