Рассуждая о булевом векторе в Coq, исходя из значения его суммы. (вид универсальной реализации для векторов) - PullRequest
Новая
       8

Рассуждая о булевом векторе в Coq, исходя из значения его суммы. (вид универсальной реализации для векторов)

0 голосов
/ 09 сентября 2018

Я застрял с теоремой, которую легко сформулировать:

«Если максимальный элемент вектора равен 0, то каждый элемент вектора равен 0».

Цель состоит в том, чтобы использовать такую ​​идиому, как "fold_left orb false v". Поэтому моя первая цель - доказать эту конкретную лемму: 

Lemma all_then_some (A:Type) : 
 forall (n:nat) (p:Fin.t (S n))
  (v : Vector.t bool (S n))
  (H : (Vector.fold_left orb false v) = false), 
 (Vector.nth v p) = false.
Proof.
...

Некоторые мысли:

1) Чтобы укрепить гипотезу и доказать что-то вроде этого: 

(forall (b:bool), (List.fold_left orb l b)  = b) <->
(forall (p:nat), (List.nth p l false) = false)
(** NB: variant for lists here! **)

2) Использовать принцип "rectS" из стандартной библиотеки / Vectors / Fin.v

3) Использовать небольшую библиотеку отражений.

ОБНОВЛЕНИЕ: чтобы найти частичное решение, смотрите мой ответ ниже. (Ged)

ОБНОВЛЕНИЕ 2: Решение здесь: https://github.com/georgydunaev/TRASH/blob/master/UNIV_INST.v (это называется "Теорема all_then_someV")

Ответы [ 2 ]

0 голосов
/ 11 сентября 2018

Код состоит из двух частей: Я доказал свою лемму для Списка в 1-ой части и, аналогично, я почти доказал для Вектора во 2-ой части. Проблема в последнем шаге второй части. («индукция р.» вызывает «Абстрагирование от терминов« n0 »и« р »приводит к термину… который неправильно напечатан». Я не понимаю, что мне делать вместо «индукции р.».) 

(*PART 1*)
Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint A2 l :fold_left orb l true = true.
Proof.
destruct l; simpl.
reflexivity.
apply A2.
Defined.

Theorem A1 (x y:bool): (orb x y = false)->(x=false)/\(y=false).
Proof. intro H. destruct x, y; firstorder || inversion H. Defined.

Fixpoint A0 b l : fold_left orb (b :: l) false = orb b (fold_left orb l false) .
Proof.
destruct l.
simpl. firstorder.
simpl.
destruct b.
simpl.
apply A2.
simpl.
reflexivity.
Defined.

Fixpoint all_then_some (l:list bool) {struct l}:
(List.fold_left orb l false) = false ->
(forall (p:nat), (List.nth p l false) = false).
Proof.
intros.
destruct l. simpl. destruct p; trivial.
simpl.
rewrite A0 in H.
pose (Q:=A1 _ _ H).
destruct Q.
destruct p. trivial.
apply all_then_some.
trivial.
Defined.
(*PART 2*)
Require Import Coq.Vectors.Vector.
Import VectorNotations.

Fixpoint B2 (n:nat) (l:t bool n) :fold_left orb true l  = true.
Proof.
destruct l; simpl.
reflexivity.
apply B2.
Defined.

Fixpoint B0 b (n:nat) (l:t bool n) : 
fold_left orb false (b :: l)  = orb b (fold_left orb false l) .
Proof.
destruct l.
simpl. firstorder.
simpl.
destruct b.
simpl.
apply B2.
simpl.
reflexivity.
Defined.

Fixpoint all_then_someV (n:nat) (l:Vector.t bool n) {struct l}:
(Vector.fold_left orb false l ) = false ->
(forall p, (Vector.nth l p  ) = false).
Proof.
intros.
induction l eqn:equa.
inversion p. (* simpl. destruct p; trivial.*)
(*simpl.*)
rewrite B0 in H.
pose (Q:=A1 _ _ H).
destruct Q.
induction p.

Я думаю, что-то вроде следующего кода может помочь (потому что тактика "destruct" похожа на "_rect" приложение), но я не уверен. 

Definition G0 h (n:nat) (l:Vector.t bool n) := fold_left orb false (h :: l) = false.
fold G0 in H.
assert (vari : G0 h n l).
exact H.
clear H.
revert h l vari.
set (P := fun n p => forall (h : bool) (l : t bool n) (_ : G0 h n l),
@eq bool (@nth bool (S n) (cons bool h n l) p) false).
unshelve eapply (@Fin.rectS P).

ОБНОВЛЕНИЕ2: Решение здесь: https://github.com/georgydunaev/TRASH/blob/master/UNIV_INST.v (это называется "Теорема all_then_someV")

0 голосов
/ 10 сентября 2018

Вы действительно можете использовать более структурированную лемму из math-comp, краткий пример [который, безусловно, можно улучшить]: 

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma nat_of_bool_inj : injective nat_of_bool.
Proof. by case=> [] []. Qed.

Lemma all_false n (r : n.-tuple bool) :
  \max_(i in 'I_n) tnth r i <= 0 ->
  forall i, tnth r i = false.
Proof.
by move/bigmax_leqP => H i; apply/nat_of_bool_inj/eqP; rewrite -leqn0 H.
Qed.

У вас есть еще несколько специализированных лемм, касающихся \big[orb/false] с has.

...