Как развернуть точку фиксации Coq за одну итерацию - PullRequest
Новая
       7

Как развернуть точку фиксации Coq за одну итерацию

0 голосов
/ 30 декабря 2018

У меня есть следующее в моей среде доказательства: 

1 subgoal
a, b : nat
H : (fix loop (m : nat) : nat :=
       match (m - a) with
       | 0 => m
       | S m' => loop m'
       end) b = 0
G : (b - a) = 0

Ясно, что H эквивалентно 

       match (b - a) with
       | 0 => b
       | S m' => loop m'
       end = 0

, что позволило бы мне переписать, используя G.

Но так как он заперт там, представлен как (m - a), я не могу переписать, используя G.

Как развернуть точку фиксации за одну итерацию?

Редактировать:следующий код создаст среду проверки.Просто игнорируйте заявления о признании.Ваша цель не в том, чтобы доказать утверждение (что тривиально), а в том, чтобы «раскрыть» точку фиксации. 

From mathcomp Require Import all.

Goal forall a b : nat,
  modn b a = 0 -> True.
Proof.
  intros a b H.
  unfold modn in H.
  destruct a.
    + admit.
    + simpl in H.
      assert ((b - a) = 0) as G.
      - admit.
      - unfold modn_rec in H.

1 Ответ

0 голосов
/ 30 декабря 2018

Чтобы развернуть точку фиксации, вам нужно уничтожить ее убывающий аргумент. 

destruct b; simpl in H.

Если вы хотите сохранить один случай, вам придется доказать равенство, которое вы упоминаете, в отдельной лемме или assert ион. 

assert (Hfix : (fix loop m := match ... end) b = match ... end)
...