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
|
(** * Lift foralls out of sig proofs *)
Definition lift1_sig {A C} (P:A->C->Prop)
(op_sig : forall (a:A), {c | P a c})
: { op : A -> C | forall (a:A), P a (op a) }
:= exist
(fun op => forall a, P a (op a))
(fun a => proj1_sig (op_sig a))
(fun a => proj2_sig (op_sig a)).
Definition lift2_sig {A B C} (P:A->B->C->Prop)
(op_sig : forall (a:A) (b:B), {c | P a b c})
: { op : A -> B -> C | forall (a:A) (b:B), P a b (op a b) }
:= exist
(fun op => forall a b, P a b (op a b))
(fun a b => proj1_sig (op_sig a b))
(fun a b => proj2_sig (op_sig a b)).
Definition lift3_sig {A B C D} (P:A->B->C->D->Prop)
(op_sig : forall (a:A) (b:B) (c:C), {d | P a b c d})
: { op : A -> B -> C -> D | forall (a:A) (b:B) (c:C), P a b c (op a b c) }
:= exist
(fun op => forall a b c, P a b c (op a b c))
(fun a b c => proj1_sig (op_sig a b c))
(fun a b c => proj2_sig (op_sig a b c)).
Definition lift4_sig {A B C D E} (P:A->B->C->D->E->Prop)
(op_sig : forall (a:A) (b:B) (c:C) (d:D), {e | P a b c d e})
: { op : A -> B -> C -> D -> E | forall (a:A) (b:B) (c:C) (d:D), P a b c d (op a b c d) }
:= exist
(fun op => forall a b c d, P a b c d (op a b c d))
(fun a b c d => proj1_sig (op_sig a b c d))
(fun a b c d => proj2_sig (op_sig a b c d)).
Definition lift4_sig_sig {A B C D E} {E' : A -> B -> C -> D -> E -> Prop}
(P:forall (a:A) (b:B) (c:C) (d:D) (e:E), E' a b c d e -> Prop)
(op_sig : forall (a:A) (b:B) (c:C) (d:D), {e : {e : E | E' a b c d e } | P a b c d (proj1_sig e) (proj2_sig e) })
(opTP := fun op : A -> B -> C -> D -> E => forall a b c d, E' a b c d (op a b c d))
: { op : sig opTP
| forall (a:A) (b:B) (c:C) (d:D), P a b c d (proj1_sig op a b c d) (proj2_sig op a b c d) }
:= exist
(fun op : sig opTP => forall a b c d, P a b c d (proj1_sig op a b c d) (proj2_sig op a b c d))
(exist opTP (fun a b c d => proj1_sig (proj1_sig (op_sig a b c d))) (fun a b c d => proj2_sig (proj1_sig (op_sig a b c d))))
(fun a b c d => proj2_sig (op_sig a b c d)).
|
