42 lines
1.1 KiB
Text
42 lines
1.1 KiB
Text
|
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.
|