| Server IP : 127.0.1.1 / Your IP : 216.73.216.152 Web Server : Apache/2.4.52 (Ubuntu) System : Linux bahcrestlinepropertiesllc 5.15.0-113-generic #123-Ubuntu SMP Mon Jun 10 08:16:17 UTC 2024 x86_64 User : www-data ( 33) PHP Version : 7.4.33 Disable Function : pcntl_alarm,pcntl_fork,pcntl_waitpid,pcntl_wait,pcntl_wifexited,pcntl_wifstopped,pcntl_wifsignaled,pcntl_wifcontinued,pcntl_wexitstatus,pcntl_wtermsig,pcntl_wstopsig,pcntl_signal,pcntl_signal_get_handler,pcntl_signal_dispatch,pcntl_get_last_error,pcntl_strerror,pcntl_sigprocmask,pcntl_sigwaitinfo,pcntl_sigtimedwait,pcntl_exec,pcntl_getpriority,pcntl_setpriority,pcntl_async_signals,pcntl_unshare, MySQL : OFF | cURL : ON | WGET : ON | Perl : ON | Python : OFF | Sudo : ON | Pkexec : ON Directory : /var/www/bahcrestline/core/vendor/scrivo/highlight.php/test/detect/coq/ |
Upload File : |
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.