Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to define the devision on nat by using Fixpoint

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to define the devision on nat by using Fixpoint


Chronological Thread 
  • 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.




Archive powered by MHonArc 2.6.18.

Top of Page