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
|
Require Import ssreflect.
Require Import List.
Lemma test_elim_pattern_1 : forall A (l:list A), l ++ nil = l.
Proof.
intros A.
elim/list_ind => [^~ 1 ].
by [].
match goal with |- (a1 :: l1) ++ nil = a1 :: l1 => idtac end.
Abort.
Lemma test_elim_pattern_2 : forall A (l:list A), l ++ nil = l.
Proof.
intros. elim: l => [^~ 1 ].
by [].
match goal with |- (a1 :: l1) ++ nil = a1 :: l1 => idtac end.
Abort.
Lemma test_elim_pattern_3 : forall A (l:list A), l ++ nil = l.
Proof.
intros. elim: l => [ | x l' IH ].
by [].
match goal with |- (x :: l') ++ nil = x :: l' => idtac end.
Abort.
Generalizable Variables A.
Class Inhab (A:Type) : Type :=
{ arbitrary : A }.
Lemma test_intro_typeclass_1 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1.
Proof.
move =>> H.
match goal with |- _ = _ => idtac end.
Abort.
Lemma test_intro_typeclass_2 : forall A `{Inhab A} (x:A), x = arbitrary -> x = arbitrary.
Proof.
move =>> H.
match goal with |- _ = _ => idtac end.
Abort.
Lemma test_intro_temporary_1 : forall A (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1.
Proof.
move => A + l2.
match goal with |- forall l1, l2 = nil -> l1 ++ l2 = l1 => idtac end.
Abort.
Lemma test_intro_temporary_2 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1.
Proof.
move => > E.
match goal with |- _ = _ => idtac end.
Abort.
Lemma test_dispatch : (forall x:nat, x= x )/\ (forall y:nat, y = y).
Proof.
intros. split => [ a | b ].
match goal with |- a = a => by [] end.
match goal with |- b = b => by [] end.
Abort.
Lemma test_tactics_as_view_1 : forall A (l1:list A), nil ++ l1 = l1.
Proof.
move => /ltac:(simpl).
Abort.
Lemma test_tactics_as_view_2 : forall A, (forall (l1:list A), nil ++ l1 = l1) /\ (nil ++ nil = @nil A).
Proof.
move => A.
(* TODO: I want to do [split =>.] as a temporary step in setting up my script,
but this syntax does not seem to be supported. Can't we have an empty ipat?
Note that I can do [split => [ | ]]*)
split => [| /ltac:(simpl)].
Abort.
Notation "%%" := (ltac:(simpl)) : ssripat_scope.
Lemma test_tactics_as_view_3 : forall A, (forall (l1:list A), nil ++ l1 = l1) /\ (nil ++ nil = @nil A).
Proof.
move => /ltac:(split) [ | /%% ].
Abort.
|
