| 1234567891011121314151617181920212223242526272829303132333435363738394041 |
- 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.
|
