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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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 ssrbool ssrfun.
Require Import TestSuite.ssr_mini_mathcomp.
Lemma test15: forall (y : nat) (x : 'I_2), y < 1 -> val x = y -> Some x = insub y.
move=> y x le_1 defx; rewrite insubT ?(leq_trans le_1) // => ?.
by congr (Some _); apply: val_inj=> /=; exact: defx.
Qed.
Axiom P : nat -> Prop.
Axiom Q : forall n, P n -> Prop.
Definition R := fun (x : nat) (p : P x) m (q : P (x+1)) => m > 0.
Inductive myEx : Type := ExI : forall n (pn : P n) pn', Q n pn -> R n pn n pn' -> myEx.
Parameter P1 : P 1.
Parameter P11 : P (1 + 1).
Parameter Q1 : forall P1, Q 1 P1.
Lemma testmE1 : myEx.
Proof.
apply: ExI 1 _ _ _ _.
match goal with |- P 1 => exact: P1 | _ => fail end.
match goal with |- P (1+1) => exact: P11 | _ => fail end.
match goal with |- forall p : P 1, Q 1 p => move=> *; exact: Q1 | _ => fail end.
match goal with |- forall (p : P 1) (q : P (1+1)), is_true (R 1 p 1 q) => done | _ => fail end.
Qed.
Lemma testE2 : exists y : { x | P x }, sval y = 1.
Proof.
apply: ex_intro (exist _ 1 _) _.
match goal with |- P 1 => exact: P1 | _ => fail end.
match goal with |- forall p : P 1, @sval _ _ (@exist _ _ 1 p) = 1 => done | _ => fail end.
Qed.
Lemma testE3 : exists y : { x | P x }, sval y = 1.
Proof.
have := (ex_intro _ (exist _ 1 _) _); apply.
match goal with |- P 1 => exact: P1 | _ => fail end.
match goal with |- forall p : P 1, @sval _ _ (@exist _ _ 1 p) = 1 => done | _ => fail end.
Qed.
Lemma testE4 : P 2 -> exists y : { x | P x }, sval y = 2.
Proof.
move=> P2; apply: ex_intro (exist _ 2 _) _.
match goal with |- @sval _ _ (@exist _ _ 2 P2) = 2 => done | _ => fail end.
Qed.
#[export] Hint Resolve P1.
Lemma testmE12 : myEx.
Proof.
apply: ExI 1 _ _ _ _.
match goal with |- P (1+1) => exact: P11 | _ => fail end.
match goal with |- Q 1 P1 => exact: Q1 | _ => fail end.
match goal with |- forall (q : P (1+1)), is_true (R 1 P1 1 q) => done | _ => fail end.
Qed.
Create HintDb SSR.
#[export] Hint Resolve P11 : SSR.
Ltac ssrautoprop := trivial with SSR.
Lemma testmE13 : myEx.
Proof.
apply: ExI 1 _ _ _ _.
match goal with |- Q 1 P1 => exact: Q1 | _ => fail end.
match goal with |- is_true (R 1 P1 1 P11) => done | _ => fail end.
Qed.
Definition R1 := fun (x : nat) (p : P x) m (q : P (x+1)) (r : Q x p) => m > 0.
Inductive myEx1 : Type :=
ExI1 : forall n (pn : P n) pn' (q : Q n pn), R1 n pn n pn' q -> myEx1.
#[export] Hint Extern 0 (Q 1 P1) => apply (Q1 P1) : SSR.
(* tests that goals in prop are solved in the right order, propagating instantiations,
thus the goal Q 1 ?p1 is faced by trivial after ?p1, and is thus evar free *)
Lemma testmE14 : myEx1.
Proof.
apply: ExI1 1 _ _ _ _.
match goal with |- is_true (R1 1 P1 1 P11 (Q1 P1)) => done | _ => fail end.
Qed.
|
