The Coq mailing list

[Pierre Cast�ran <pierre.casteran AT labri.fr>]

Hi,

  You can get a solution of the bitwise  or on binary wordsin the tutorial on
[Co]inductive types (section "A case study in dependant elimination")

http://www.labri.fr/perso/casteran


A former (quite more compact) solution can be found on
http://www.labri.fr/perso/casteran/CoqArt/structinduct/binary_word_or.html

There are also some contributions by various people in the Coq-club mailing
list archive.

Best regards,

Pierre





Quoting Joan Josep Jiménez Puig 
<jumi99 AT gmail.com>:

> Hi,
> first of all apologies for my english :) I'm reading the Coq'Art book and
> there's
> one exercise I cannot solve. It is from chapter 6, Dependent Inductive
> Types.
>
> I have defined a type (binary_word : nat -> Set) of strings of bits of a
> known length.
> The exercise is to compute the bit-wise "or" of two binary_words.
>
> Here's the code I've done, but it doesn't work because in the recursive call
> there's a problem with the parameter n. If I put x it will complain
> about the type of bw2' and if i put x' it will complain about bw1'.
> I have to use somehow the fact that x=x', but I don't know how to do it.
>
> Inductive binary_word : nat -> Set :=
>   |F : binary_word O
>   |M : forall n:nat, Bit -> binary_word n -> binary_word (S n).
>
> Fixpoint binary_word_or (n:nat) (bw1:binary_word n)
>                                 (bw2:binary_word n) {struct bw1}
>          : binary_word n :=
>    match bw1 in binary_word q return binary_word q with
>       | F => F
>       | M x b bw1' =>
>          match bw2 in binary_word q return binary_word q with
>             | F => F
>             | M x' b2 bw2' =>
>                M x (bit_or b b2) (binary_word_or x bw1' bw2')
>          end
>    end.
>
> Thanks.



Pierre Castéran