The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

In the 2004 version of the tutorial on [co]-inductive types (available 
through coq's page : http://coq.inria.fr
"Additional documentation" ) there is a case study on dependent 
elimination (p 49-54) , using a double
recursion combinator.
The attached file contains an example very similar to the statement 
given in the first mail of this thread.

Hope this helps,

Pierre





roconnor AT theorem.ca
 wrote:

> On Tue, 13 Sep 2005 
> roconnor AT theorem.ca
>  wrote:
>
>  
>
> > Think about what the two goals will be after the destruct.  Write out what
> > they are.  Then you will realize it will be neccesary to
> >
> > unfold band32.
> >    
>
> Actually now that I think about it, it is not clear from the resulting
> goals that it is neccesary to unfold band32.  Furthermore you probably
> don't want to do destruct; destruct will generalize away the 32 and
> consider both constructors.
>
> You don't want to do this.  You know your vector is of lenght 32, so you
> know there is only one possible constructor.  What you want instead is
> dependent inverison.  The solution to your 2nd order woes is seems to be
> to generalize anything related to your term.
>
> In this case you will need to do
>
> generalize e2
> clear e2
> unfold band32
> dependent inverion e1
>
> Of course the next thing you will want to do is
>
> dependent inversion e2.
>
> But how you are going to do that is beyond my skills.  I'd be tempted to
> do the whole proof via (vector (bool*bool) 32).  Perhaps others know
> better solutions.
>
> Welcome to the nightmare that is programming with dependent types. ;-)
>
>  


Require Import Bvector.


Definition xorb (b1 b2:bool) :=
match b1, b2 with 
 | false, true => true
 | true, false => true
 | _ , _       => false
end.


Definition Vtail_total 
   (A : Set) (n : nat) (v : vector A n) : vector A (pred n):=
match v in (vector _ n0) return (vector A (pred n0)) with
| Vnil => Vnil A
| Vcons _ n0 v0 => v0
end.

Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n).
 intros A n v; case v.  
 simpl.
 exact (Vnil A).
 simpl.
 auto.
Defined.



Implicit Arguments Vcons [A n].
Implicit Arguments Vnil [A].
Implicit Arguments Vhead [A n].
Implicit Arguments Vtail [A n].

Definition Vid : forall (A : Set)(n:nat), vector A n -> vector A n.
Proof.
 destruct n; intro v.
 exact Vnil.
 exact (Vcons  (Vhead v) (Vtail v)).
Defined.

Eval simpl in (fun (A:Set)(v:vector A 0) => (Vid _ _ v)).

Eval simpl in (fun (A:Set)(v:vector A 0) => v).



Lemma Vid_eq : forall (n:nat) (A:Set)(v:vector A n), v=(Vid _ n v).
Proof.
 destruct v. 
 reflexivity.
 reflexivity.
Defined.

Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
Proof.
 intros.
 change (Vnil (A:=A)) with (Vid _ 0 v). 
 apply Vid_eq.
Defined.


Theorem decomp :
  forall (A : Set) (n : nat) (v : vector A (S n)),
  v = Vcons (Vhead v) (Vtail v).
Proof.
 intros.
 change (Vcons (Vhead v) (Vtail v)) with (Vid _  (S n) v).
 apply Vid_eq.
Defined.



Definition vector_double_rect : 
    forall (A:Set) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
        P 0 Vnil Vnil ->
        (forall n (v1 v2 : vector A n) a b, P n v1 v2 ->
             P (S n) (Vcons a v1) (Vcons  b v2)) ->
        forall n (v1 v2 : vector A n), P n v1 v2.
 induction n.
 intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
 auto.
 intros v1 v2; rewrite (decomp _ _ v1);rewrite (decomp _ _ v2).
 apply X0; auto.
Defined.

Require Import Bool.

Definition bitwise_or n v1 v2 : vector bool n :=
   vector_double_rect bool  (fun n v1 v2 => vector bool n)
                        Vnil
                        (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.


Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:vector A p){struct v}
                  : option A :=
  match n,v  with
    _   , Vnil => None
  | 0   , Vcons b  _ _ => Some b
  | S n', Vcons _  p' v' => vector_nth A n'  p' v'
  end.



Implicit Arguments vector_nth [A p].


Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i  a b,
      vector_nth i v1 = Some a ->
      vector_nth i v2 = Some b ->
      vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
Proof.
 intros  n v1 v2; pattern n,v1,v2.
 apply vector_double_rect.
 simpl.
 destruct i; discriminate 1.
 destruct i; simpl;auto.
 injection 1; injection 2;intros; subst a; subst b; auto.
Qed.



Definition bodd (v:vector bool 32) :=
  vector_nth 0 v = Some true.

Definition beven (v:vector bool 32) :=
  vector_nth 0 v = Some false.

Goal forall (v1 v2: vector bool 32),
      bodd v1 /\ bodd v2  -> bodd (bitwise_or _ v1 v2).
 
 intros v1 v2 (B1,B2).
 red.
 generalize (nth_bitwise _ v1 v2 0).
 intro H.
 generalize (H _ _ B1 B2).
 
 simpl (true||true).
 auto.
Qed.