Найти наибольший общий делитель чисел m и n.
В Coq есть операция m mod n (или modulo m n), которая возвращает остаток от деления m на n. Однако поскольку все функции в Coq являются тотальными, значение выражения m mod 0 равно 0 по определению. Также есть предикат (n | m) (пишется в скобках; или divide n m), который равен True, если n делит m. Следует обратить внимание, что modulo возвращает nat и следовательно может быть использован в программах, в то время как divide n m возвращает Prop и может использоваться только в спецификациях. Не забывайте использовать инструкции import, определение тактики bdestruct и пример нахождение максимума массива , которые находятся ниже.
Require Import Arith.
Require Import Lia.
Require Import Bool.
Import Nat Peano.
Search le.
Global Hint Resolve ltb_spec0 leb_spec0 eqb_spec : bdestruct.
Ltac bdestr X H :=
let e := fresh "e" in
evar (e : Prop);
assert (H : reflect e X); subst e;
[ eauto with bdestruct
| destruct H as [H | H];
[ | try first [apply nlt_ge in H | apply nle_gt in H]]].
Tactic Notation "bdestruct" constr(X) := let H := fresh in bdestr X H.
Tactic Notation "bdestruct" constr(X) "as" ident(H) := bdestr X H.
Section ArrayMax.
Variable array : nat -> nat.
( [arrayMax n] возвращает [max(array 0, ..., array n)]. Массив
непустой для любого n >= 0, поэтому максимум определен. *)
Fixpoint arrayMax (n : nat) : nat :=
match n with
| 0 => array 0
| S k => max (arrayMax k) (array n)
end.
Theorem arrayMaxSpec1 :
forall n i, i <= n -> array i <= arrayMax n.
Proof.
induction n as [| n IH]; intros i H.
* assert (H1 : i = 0) by lia. rewrite H1. reflexivity.
( Тактика [reflexivity] доказывает не только [M = M],
но и [M <= M]. *)
* assert (H1 : i <= n \/ i = S n) by lia.
clear H.
( Эта посылка больше не нужна. *)
simpl.
( Упрощение [arrayMax (S n)] по определению. *)
destruct H1 as [H1 | H1].
+ apply (le_trans _ (arrayMax n)).
- auto.
( Следует непосредственно из предположения индукции. *)
- apply le_max_l.
+ subst i.
( Или [rewrite H1]. *)
apply le_max_r.
Qed.
Check le_trans.
Fixpoint arrayMax' (n : nat) : nat :=
match n with
| 0 => array 0
| S k => let p := arrayMax' k in
if p <=? array n then array n else p
end.
Theorem arrayMaxSpec1' :
forall n i, i <= n -> array i <= arrayMax' n.
Proof.
induction n as [| n IH]; intros i H.
* assert (H1 : i = 0) by lia. now rewrite H1.
* assert (H1 : i <= n \/ i = S n) by lia; clear H.
simpl. destruct H1 as [H1 | H1].
+ apply (le_trans _ (arrayMax' n)).
- auto.
- bdestruct (arrayMax' n <=? array (S n)) as H.
-- assumption.
-- reflexivity.
+ subst i.
bdestruct (arrayMax' n <=? array (S n)) as H.
- easy.
- now apply lt_le_incl.
Qed.
Lemma max_variants : forall m n, max m n = m \/ max m n = n.
Proof.
Admitted.
Theorem arrayMaxSpec2 :
forall n, exists i, i <= n /\ array i = arrayMax n.
Proof.
Admitted.
Fixpoint arrayMaxHelp (n p : nat) : nat :=
match n with
| 0 => max p (array 0)
| S k => arrayMaxHelp k (max p (array n))
end.
Definition arrayMax1 (n : nat) : nat := arrayMaxHelp n (array n).
(** Докажите равенство функций arrayMax и arrayMax1 *)
Theorem maxEqual : forall n, arrayMax n = arrayMax1 n.
Admitted.
End ArrayMax.