mqpCoq2018/RewritingDefinitions.v at master · dandougherty/mqpCoq2018 · 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
70
71
72
73
74
75
76
77
78

(* Unfolding a recursive definition is usually a mess.  Here is a
little trick that addresses this.
*)

(** Here is a dumb thing to prove, as an example *)


Fixpoint fact n :=
  match n with
    | 0   => 1
    | S n => (S n) * fact n
  end.

Goal
  forall (f: nat -> nat) (n: nat),
    f (fact (S n) ) = f ((S n) * fact n).
Proof.
  intros f n.
  unfold fact.
  (* UGH! *)
  Abort.

(* What we really want to do is REWRITE with (the second clause of)
the definition of fact, as opposed to unfod.

Unfortunately, Coq won't let you rewrite with definitions.  The trick
is to make a Lemma capturing the definition.  Such a lemma should be
easy to prove:

*)

Lemma lfact :
  forall n, fact n =   match n with
                       | 0   => 1
                       | S n => (S n) * fact n
                       end.
Proof.
  intros.
  induction n as [| m].
  -  reflexivity.
  -  unfold fact.
     reflexivity.
Qed.


(* Now our proof is easy *)

Goal
  forall (f: nat -> nat) (n: nat),
    f (fact (S n) ) = f ((S n) * fact n).
Proof.
    intros.
    rewrite lfact.
    reflexivity.
  Qed.

(* Another approach is to make each clause a lemma.  More direct
   somehow, though (even) more verbose.

   I suspect that with functions more complex than fact this might work
  better (?).

 *)

Lemma fact0 : fact 0 = 1.
Proof. reflexivity. Qed.

Lemma factS n : fact (S n) = (S n) * fact n.
Proof. reflexivity. Qed.

Goal
  forall (f: nat -> nat) (n: nat),
    f (fact (S n) ) = f ((S n) * fact n).
Proof.
  intros f n.
  rewrite factS.  reflexivity.
Qed.