The Coq mailing list

[Paul Tarau <paul.tarau AT gmail.com>]

(* This has turned now into a fairly complete implementation of
bijective base-2 arithmetic, combined with a bijective Goedel
numbering scheme for sets and lists - using exclusively structural
induction:

http://logic.csci.unt.edu/tarau/research/2011/Bij2.v.txt.

Comments on the code are welcome - I am and I will be forever a beginner :-)

My next challenge is to describe arithmetic computations directly on
binary trees - a kind of hereditary base 2 exponent notation - as used
in Goodstein's theorem). It is interesting because it allows computing
with gigantic numbers that binary representations cannot handle. The
intuition is that the first argument of the constructor C represents
an exponent of 2, recursively
*)

Inductive T : Set :=
| E : T
| C : T -> T -> T.

Delimit Scope T_scope with T.
Bind Scope T_scope with T.
Arguments Scope T [T_scope].

Fixpoint exp2 (x: nat) : nat :=
match x with
| 0 => S 0
| S n => 2*(exp2 n)
end.

(* a bijection from T to nat *)
Fixpoint t2n (t : T) {struct t} : nat :=
match t with
| E => 0
| C x y => (exp2 (t2n x)) * (2*(t2n y)+1)
end.

Eval compute in t2n (C (C E E) (C E E)).

(* mutually recursive components of s,p *)
Fixpoint s0 (a:T) :=
match a with
| E => E
| (C E y) => C (s0 (s0 y)) (s1 (s0 y))
| (C (C _ _) _) => E
end
with s1 (a:T) :=
match a with
| E => E
| (C E y) => s1 y
| (C (C a b) y) => C (p2 a b) y
end
with p2 (x:T) (y:T) :=
match x,y with
| E,E => E
| E,(C a b) => C (C (s0 a) (s1 a)) b
| (C a b),c => C E (p2 (p2 a b) c)
end.

(* successor on T such that t2n mapps it into x->x+1 on nat *)
Definition s(a:T) := C (s0 a) (s1 a).

(* predecessor on T such that t2n mapps it predecessor on nat *)
Definition p(a:T) :=
match a with
| E => E (* pro forma - just to make it total *)
| C x y => p2 x y
end.

(*
Unfortunately, Coq rejects this with:

Error: Cannot guess decreasing argument of fix.

I think that termination of the mutually recursive Fixpoint
follows from the fact that at each step in every match
in every definition at least one argument becomes structurally
simpler - so every reduction in the mutually recursive
definition makes progress towards termination.

Is it the mutual recursion that confuses Coq? Doest it make sense to
use the bijection to nat "t2n" as a measure? Defining a well founded
relation seems tricky as one needs successor/predecessor to work
first.

P.S. The Haskell equivalent works as expected so it is unlikely that I
have any logical erros in my definition. Here it is:

data T = E|C T T deriving (Eq,Read,Show)

s0 E = E
s0 (C E y) = C (s0 (s0 y)) (s1 (s0 y))
s0 (C (C _ _) _) = E

s1 E = E
s1 (C E y) = s1 y
s1 (C (C a b) y) = C (p2 a b) y

p2 E E = E
p2 E (C a b) = C (C (s0 a) (s1 a)) b
p2 (C a b) y = C E (p2 (p2 a b) y)

-- successor and predecessor on type T
s x = C (s0 x) (s1 x)
p (C x y) = p2 x y

-- nat to T conversion
n2t 0 = E
n2t x | x>0 = s (n2t (x-1))

-- T to nat conversion
t2n E = 0
t2n (C x y) = 2^(t2n x)*(2*(t2n y)+1)

-- tests
check = map (t2n.n2t) [0..31]
pcheck = map (t2n.p.s.n2t) [0..31]

*)

(*
On Sat, May 28, 2011 at 2:01 PM, Paul Tarau 
<paul.tarau AT gmail.com>
 wrote:
> Thanks for you help - the following did it:
> Lemma sp_inv : forall n:B, p (s n) = n.
> Proof.
> induction n.
> intros;firstorder.
> trivial.
> rewrite psi_os.
> rewrite pos_ips.
> f_equal. trivial.
> Qed.
> Paul
> On May 28, 2011, at 1:14 PM, Guillaume Brunerie wrote:
>
>
> 2011/5/28 Paul Tarau 
> <paul.tarau AT gmail.com>
>>
>> I would like Coq to reason along the following equations:
>>     p (s (i b)) = p (o (s b)) = i (p (s b)) = i b
>> where I want to use, as an inductive hypothesis, that p (s b) = b holds.
>> I tried "apply psi_os" (that I just proved) but it seems to want both
>> sides
>> of an equation - is there any way to make it just rewrite p (s (i b)) as
>> p (o (s b)) according to Lemma psi_os?
>
> The answer is in the question :-)
> The tactic you want is called 'rewrite', if you use 'rewrite psi_os' instead
> of 'apply psi_os', this will work (the tactic 'apply' try to match the
> current goal with the conclusion, here this is not what you want).
> In order to do an induction, you will first need to use 'induction n' at the
> beginning of the proof, and prove the two other (easy) cases of the
> induction.
>
> Guillaume
>
>
*)