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
|
<h2>Full example</h2>
<pre><code>(* Source: https://coq.inria.fr/a-short-introduction-to-coq *)
Inductive seq : nat -> Set :=
| niln : seq 0
| consn : forall n : nat, nat -> seq n -> seq (S n).
Fixpoint length (n : nat) (s : seq n) {struct s} : nat :=
match s with
| niln => 0
| consn i _ s' => S (length i s')
end.
Theorem length_corr : forall (n : nat) (s : seq n), length n s = n.
Proof.
intros n s.
(* reasoning by induction over s. Then, we have two new goals
corresponding on the case analysis about s (either it is
niln or some consn *)
induction s.
(* We are in the case where s is void. We can reduce the
term: length 0 niln *)
simpl.
(* We obtain the goal 0 = 0. *)
trivial.
(* now, we treat the case s = consn n e s with induction
hypothesis IHs *)
simpl.
(* The induction hypothesis has type length n s = n.
So we can use it to perform some rewriting in the goal: *)
rewrite IHs.
(* Now the goal is the trivial equality: S n = S n *)
trivial.
(* Now all sub cases are closed, we perform the ultimate
step: typing the term built using tactics and save it as
a witness of the theorem. *)
Qed.
</code></pre>
|
