PUMPKIN-PATCH/plugin/coq/Variants1.v at master · uwplse/PUMPKIN-PATCH · GitHub

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
(* Variants for first proof *)

Require Import Arith NPeano.

(*
   Things we can change:
   1. Outside/inside induction
   2. Apply to conclusion/apply to hypothesis/both
   3. Apply function/use hint or rewrite db/use special tactic
*)

(* Try all pairs of old and new, see what happens *)

Theorem new1:
  forall (n m p : nat),
    n <= m ->
    m <= p ->
    n <= p.
Proof.
  intros. induction H0; auto.
Qed.

(* Variant 1: Outside, conclusion, function *)

Theorem old1_v1:
  forall (n m p : nat),
    n <= m ->
    m <= p ->
    n <= p + 1.
Proof.
  intros. apply le_plus_trans. induction H0; auto.
Qed.

(* Variant 2: Inside, conclusion, function *)

Theorem old1_v2:
  forall (n m p : nat),
    n <= m ->
    m <= p ->
    n <= p + 1.
Proof.
  intros. induction H0.
  - auto with arith.
  - constructor. auto.
Qed.

(* Variant 3: Outside, conclusion, rws [1] *)

Theorem old1_v3:
  forall (n m p : nat),
    n <= m ->
    m <= p ->
    n <= p + 1.
Proof.
  intros. rewrite le_plus_trans; auto. induction H0; auto.
Qed.

(* Variant 4: Inside, conclusion, rw [2] *)

Theorem old1_v4:
  forall (n m p : nat),
    n <= m ->
    m <= p ->
    n <= p + 1.
Proof.
  intros. induction H0.
  - rewrite le_plus_trans; auto.
  - constructor. auto.
Qed.