coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: fengsheng <fsheng1990 AT 163.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] How to define the devision on nat by using Fixpoint
- Date: Wed, 19 Dec 2012 23:20:52 -0500
Here's one way to do it. There's probably an easier way, such that the proof that the halving function does what it says it does is simpler...
Inductive even_nat :=
| O_even : even_nat
| S_even : odd_nat -> even_nat
with odd_nat :=
| S_odd : even_nat -> odd_nat.
Fixpoint even_nat_to_nat (n : even_nat) : nat :=
match n with
| O_even => O
| S_even n' => S (odd_nat_to_nat n')
end
with odd_nat_to_nat (n : odd_nat) : nat :=
match n with
| S_odd n' => S (even_nat_to_nat n')
end.
Fixpoint half_even (n : even_nat) : nat :=
match n with
| O_even => O
| S_even (S_odd n') => S (half_even n')
end.
Fixpoint is_even (n : nat) : bool :=
match n with
| O => true
| S n' => negb (is_even n')
end.
Fixpoint nat_to_even_odd_nat (n : nat) : if is_even n then even_nat else odd_nat :=
match n as n0 return (if is_even n0 return Set then even_nat else odd_nat) with
| 0 => O_even
| S n' => (if is_even n' as b0
return
((if b0 then even_nat else odd_nat) ->
if negb b0 then even_nat else odd_nat)
then
S_odd
else
S_even)
(nat_to_even_odd_nat n')
end.
Definition odd_pred (n : odd_nat) : even_nat :=
match n with
| S_odd n' => n'
end.
Definition floor_half_nat (n : nat) : nat :=
half_even
((if is_even n as b0
return ((if b0 then even_nat else odd_nat) -> even_nat)
then (fun x => x)
else odd_pred) (nat_to_even_odd_nat n)).
On Wed, Dec 19, 2012 at 10:17 PM, fengsheng <fsheng1990 AT 163.com> wrote:
when I wrote a function to convert natural numbers to binary numbers,I met a
problem:how to take the value of a number half.
- [Coq-Club] How to define the devision on nat by using Fixpoint, fengsheng, 12/20/2012
- Re: [Coq-Club] How to define the devision on nat by using Fixpoint, Jason Gross, 12/20/2012
- Re: [Coq-Club] How to define the devision on nat by using Fixpoint, AUGER Cédric, 12/20/2012
- Re: [Coq-Club] How to define the devision on nat by using Fixpoint, Adam Chlipala, 12/20/2012
- Re: [Coq-Club] How to define the devision on nat by using Fixpoint, AUGER Cédric, 12/20/2012
- Re: [Coq-Club] How to define the devision on nat by using Fixpoint, Adam Chlipala, 12/20/2012
Archive powered by MHonArc 2.6.18.