The Coq mailing list

[S3 <scubed2 AT gmail.com>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

I finally got a simple form of it to work.
In the book, you used a separate function
to handle "all in list", which makes it a
bit different from the way induction normally is.
This works without the extra step,
and is close to what you would get if you just
did induction twice, except covering the 1
extra case that is impossible otherwise.

Definition BlueTree_list_ind
  (P : BlueTree -> Prop)
  (CBlue : P BlueLeaf)
  (CRed : P RedLeaf)
  (CNil : P (Branch nil))
  (CBranch : (forall a b, P a -> P (Branch b) -> P (Branch (a::b))))
  (t : BlueTree)
  : P t := (
fix outer (b : BlueTree) : P b :=
  match b as b0 return (P b0) with
  | BlueLeaf => CBlue
  | RedLeaf => CRed
  | Branch l => (
      fix inner (l0 : list BlueTree) : P (Branch l0) :=
        match l0 with
        | nil => CNil
        | h0 :: t0 => CBranch h0 t0 (outer h0) (inner t0)
        end
      ) l
  end
) t.

- -- 
$_="sccc,gB1,a_oo,JosBackuSa,g11,ug1a,oscc,cBBg,JcgaBuucaB_s11_Juc_c";
while(($c,$b,$a)=m/^(.)([^,]*),(.*)$/){$_=$a;s/$c/$b/g;}
print map chr length,split /_/;
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk+5bVcACgkQxzVgPqtIcfsEAACfdrhAthwvl8wwO4I63Ba0VKMt
T/8AnRQdhPeCRuVD+V0tHSrPx90wd6E+
=bXNW
-----END PGP SIGNATURE-----