1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
Require Import Coq.Vectors.Vector.
Axiom exfalso : False.
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.
destruct l.
inversion p.
revert h l H.
set (P := fun n p => forall (h : bool) (l : t bool n),
fold_left orb false (cons bool h n l) = false -> @eq bool (@nth bool (S n) (cons bool h n l) p) false).
revert n p.
fix loop 1.
unshelve eapply (@Fin.rectS P).
+ elim exfalso.
+ unfold P.
intros.
eapply all_then_someV.
exact H0.
Fail Defined.
Abort.
|
