blob: c7c20d8f8b7e1c2bd43518fec495a75a991b16e2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
Require Import ssreflect.
Require Import ssrbool TestSuite.ssr_mini_mathcomp.
(* div fintype finfun path bigop. *)
Axiom daemon : False. Ltac myadmit := case: daemon.
Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F :
let s := \big[op/idx]_(i <- r | P i) F i in
K s * K' s -> K' s.
Proof. by move=> /= [_]. Qed.
Arguments big_load [R] K [K' idx op I r P F].
Section Elim1.
Variables (R : Type) (K : R -> Type) (f : R -> R).
Variables (idx : R) (op op' : R -> R -> R).
Hypothesis Kid : K idx.
Ltac ASSERT1 := match goal with |- (K idx) => myadmit end.
Ltac ASSERT2 K := match goal with |- (forall x1 : R, R ->
forall y1 : R, R -> K x1 -> K y1 -> K (op x1 y1)) => myadmit end.
Lemma big_rec I r (P : pred I) F
(Kop : forall i x, P i -> K x -> K (op (F i) x)) :
K (\big[op/idx]_(i <- r | P i) F i).
Proof.
elim/big_ind2: {-}_.
ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4.
elim/big_ind2: _ / {-}_.
ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4.
elim/big_rec2: (\big[op/idx]_(i <- r | P i) op idx (F i))
/ (\big[op/idx]_(i <- r | P i) F i).
ASSERT1. match goal with |- (forall i : I, R -> forall y2 : R, is_true (P i) -> K y2 -> K (op (F i) y2)) => myadmit end. Undo 3.
elim/(big_load (phantom R)): _.
Undo.
Fail elim/big_rec2: {2}_.
elim/big_rec2: (\big[op/idx]_(i <- r | P i) F i)
/ {1}(\big[op/idx]_(i <- r | P i) F i).
Undo.
elim/(big_load (phantom R)): _.
Undo.
Fail elim/big_rec2: _ / {2}(\big[op/idx]_(i <- r | P i) F i).
Admitted.
Definition morecomplexthannecessary A (P : A -> A -> Prop) x y := P x y.
Lemma grab A (P : A -> A -> Prop) n m : (n = m) -> (P n n) -> morecomplexthannecessary A P n m.
by move->.
Qed.
Goal forall n m, m + (n + m) = m + (n * 1 + m).
Proof. move=> n m; elim/grab : (_ * _) / {1}n => //; exact: muln1. Qed.
End Elim1.
|
