rpms/coq/devel README.coq-emacs, NONE, 1.1 RecTutorial.v, NONE, 1.1 check.patch, NONE, 1.1 cmxa-install.patch, NONE, 1.1 coq-icon.png, NONE, 1.1 coq.spec, NONE, 1.1 coqide.desktop, NONE, 1.1 import.log, NONE, 1.1 makefile-strip.patch, NONE, 1.1 makefile.patch, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2

[Alan Dunn (amdunn)]

Author: amdunn

Update of /cvs/pkgs/rpms/coq/devel
In directory cvs-int.fedora.redhat.com:/tmp/cvs-serv6819/devel

Modified Files:
	.cvsignore sources 
Added Files:
	README.coq-emacs RecTutorial.v check.patch cmxa-install.patch 
	coq-icon.png coq.spec coqide.desktop import.log 
	makefile-strip.patch makefile.patch 
Log Message:
Initial add of supporting files for coq package.



--- NEW FILE README.coq-emacs ---
This is the Fedora coq-emacs package, which includes an emacs elisp file for usage with editing Coq .v files.

--- NEW FILE RecTutorial.v ---
Check (forall A:Type, (exists x:A, forall (y:A), x <> y) -> 2 = 3).



Inductive nat : Set := 
 | O : nat 
 | S : nat->nat.
Check nat.
Check O.
Check S.

Reset nat.
Print nat.


Print le.

Theorem zero_leq_three: 0 <= 3.

Proof.
 constructor 2. 
 constructor 2.  
 constructor 2.
 constructor 1.

Qed.

Print zero_leq_three.


Lemma zero_leq_three': 0 <= 3.
 repeat constructor.
Qed.


Lemma zero_lt_three : 0 < 3.
Proof.
 repeat constructor. 
Qed.

Print zero_lt_three.
Require Import Relations.

Locate clos_trans.
(* alternate definition in style prior to V8.1 *)

Section Transitive_Closure.
  Variable A : Type.
  Variable R : relation A.

  Inductive clos_trans : A -> A -> Prop :=
    | t_step : forall x y:A, R x y -> clos_trans x y
    | t_trans :
        forall x y z:A, clos_trans x y -> clos_trans y z -> clos_trans x z.
End Transitive_Closure.
Require Import List.

Print list.

Check list.

Check (nil (A:=nat)).

Check (nil (A:= nat -> nat)).

Check (fun A: Type => (cons (A:=A))).

Check (cons 3 (cons 2 nil)).

Check (nat :: bool ::nil).

Check ((3<=4) :: True ::nil).

Check (Prop::Set::nil).

Require Import Bvector.

Print vector.

Check (Vnil nat).

Check (fun (A:Type)(a:A)=> Vcons _ a _ (Vnil _)).

Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).

Lemma eq_3_3 : 2 + 1 = 3.
Proof.
 reflexivity.
Qed.
Print eq_3_3.

Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4).
Proof.
 reflexivity.
Qed.
Print eq_proof_proof.

Lemma eq_lt_le : ( 2 < 4) = (3 <= 4).
Proof.
 reflexivity.
Qed.

Lemma eq_nat_nat : nat = nat.
Proof.
 reflexivity.
Qed.

Lemma eq_Set_Set : Set = Set.
Proof.
 reflexivity.
Qed.

Lemma eq_Type_Type : Type = Type.
Proof.
 reflexivity.
Qed.


Check (2 + 1 = 3).


Check (Type = Type).

Goal Type = Type.
reflexivity.
Qed.


Print or.

Print and.


Print sumbool.

Print ex.

Require Import ZArith.
Require Import Compare_dec.

Check le_lt_dec.

Definition max (n p :nat) := match le_lt_dec n p with 
                             | left _ => p
                             | right _ => n
                             end.

Theorem le_max : forall n p, n <= p -> max n p = p.
Proof.
 intros n p ; unfold max ; case (le_lt_dec n p); simpl.
 trivial.
 intros; absurd (p < p); eauto with arith.
Qed.

Extraction max.






Inductive tree(A:Type)   : Type :=
    node : A -> forest A -> tree A 
with
  forest (A: Type)    : Type := 
    nochild  : forest A |
    addchild : tree A -> forest A -> forest A.





Inductive 
  even    : nat->Prop :=
    evenO : even  O |
    evenS : forall n, odd n -> even (S n)
with
  odd    : nat->Prop :=
    oddS : forall n, even n -> odd (S n).

Lemma odd_49 : odd (7 * 7).
 simpl; repeat constructor.
Qed.



Definition nat_case := 
 fun (Q : Type)(g0 : Q)(g1 : nat -> Q)(n:nat) =>
    match n return Q with
    | 0 => g0 
    | S p => g1 p 
    end.

Eval simpl in (nat_case nat 0 (fun p => p) 34).

Eval simpl in (fun g0 g1 => nat_case nat g0 g1 34).

Eval simpl in (fun g0 g1 => nat_case nat g0 g1 0).


Definition pred (n:nat) := match n with O => O | S m => m end.

Eval simpl in pred 56.

Eval simpl in pred 0.

Eval simpl in fun p => pred (S p).


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


 Definition pred_spec (n:nat) := {m:nat | n=0 /\ m=0  \/ n = S m}.
  

 Definition predecessor : forall n:nat, pred_spec n.
  intro n;case n.
  unfold pred_spec;exists 0;auto.
  unfold pred_spec; intro n0;exists n0; auto.
 Defined.

Print predecessor.

Extraction predecessor.

Theorem nat_expand : 
  forall n:nat, n = match n with 0 => 0 | S p => S p end.
 intro n;case n;simpl;auto.
Qed.

Check (fun p:False => match p return 2=3 with end).

Theorem fromFalse : False -> 0=1.
 intro absurd. 
 contradiction.
Qed.

Section equality_elimination.
 Variables (A: Type)
           (a b : A)
           (p : a = b)
           (Q : A -> Type).
 Check (fun H : Q a =>
  match p in (eq _  y) return Q y with
     refl_equal => H
  end).

End equality_elimination.

           
Theorem trans : forall n m p:nat, n=m -> m=p -> n=p.
Proof.
 intros n m p eqnm.  
 case eqnm.
 trivial.        
Qed.

Lemma Rw :  forall x y: nat, y = y * x -> y * x * x = y.
 intros x y e; do 2 rewrite <- e.
 reflexivity.
Qed.


Require Import Arith.

Check mult_1_l.
(*
mult_1_l
     : forall n : nat, 1 * n = n
*)

Check mult_plus_distr_r.
(*
mult_plus_distr_r
     : forall n m p : nat, (n + m) * p = n * p + m * p

*)

Lemma mult_distr_S : forall n p : nat, n * p + p = (S n)* p.
 simpl;auto with arith.
Qed.

Lemma four_n : forall n:nat, n+n+n+n = 4*n.
 intro n;rewrite <- (mult_1_l n).

 Undo.
 intro n; pattern n at 1.
 

 rewrite <- mult_1_l.
 repeat rewrite   mult_distr_S.
 trivial.
Qed.


Section Le_case_analysis.
 Variables (n p : nat)
           (H : n <= p)
           (Q : nat -> Prop)
           (H0 : Q n)
           (HS : forall m, n <= m -> Q (S m)).
 Check (
    match H in (_ <= q) return (Q q)  with
    | le_n => H0
    | le_S m Hm => HS m Hm
    end
  ).


End Le_case_analysis.


Lemma predecessor_of_positive : forall n, 1 <= n ->  exists p:nat, n = S p.
Proof.
 intros n  H; case H.
 exists 0; trivial.
 intros m Hm; exists m;trivial.
Qed.

Definition Vtail_total 
   (A : Type) (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:Type)(n:nat)(v:vector A n) : vector A (pred n).
 intros A n v; case v.  
 simpl.
 exact (Vnil A).
 simpl.
 auto.
Defined.

(*
Inductive Lambda : Set :=
  lambda : (Lambda -> False) -> Lambda. 


Error: Non strictly positive occurrence of "Lambda" in
 "(Lambda -> False) -> Lambda"

*)

Section Paradox.
 Variable Lambda : Set.
 Variable lambda : (Lambda -> False) ->Lambda.

 Variable matchL  : Lambda -> forall Q:Prop, ((Lambda ->False) -> Q) -> Q.
 (*
  understand matchL Q l (fun h : Lambda -> False => t)

  as match l return Q with lambda h => t end 
 *)

 Definition application (f x: Lambda) :False :=
   matchL f False (fun h => h x).

 Definition Delta : Lambda := lambda (fun x : Lambda => application x x).

 Definition loop : False := application Delta Delta.

 Theorem two_is_three : 2 = 3.
 Proof.
  elim loop.
 Qed.

End Paradox.


Require Import ZArith.



Inductive itree : Set :=
| ileaf : itree
| inode : Z-> (nat -> itree) -> itree.

Definition isingle l := inode l (fun i => ileaf).

Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))).

Definition t2 := inode 0 
                      (fun n : nat => 
                               inode (Z_of_nat n)
                                     (fun p => isingle (Z_of_nat (n*p)))).


Inductive itree_le : itree-> itree -> Prop :=
  | le_leaf : forall t, itree_le  ileaf t
  | le_node  : forall l l' s s', 
                       Zle l l' -> 
                      (forall i, exists j:nat, itree_le (s i) (s' j)) -> 
                      itree_le  (inode  l s) (inode  l' s').


Theorem itree_le_trans : 
  forall t t', itree_le t t' ->
               forall t'', itree_le t' t'' -> itree_le t t''.
 induction t.
 constructor 1.
 
 intros t'; case t'.
 inversion 1.
 intros z0 i0 H0.
 intro t'';case t''.
 inversion 1.
 intros.
 inversion_clear H1.
 constructor 2.
 inversion_clear H0;eauto with zarith.
 inversion_clear H0.
 intro i2; case (H4 i2).
 intros.
 generalize (H i2 _ H0). 
 intros.
 case (H3 x);intros.
 generalize (H5 _ H6).
 exists x0;auto.
Qed.

 

Inductive itree_le' : itree-> itree -> Prop :=
  | le_leaf' : forall t, itree_le'  ileaf t
  | le_node' : forall l l' s s' g, 
                       Zle l l' ->  
                      (forall i, itree_le' (s i) (s' (g i))) -> 
                       itree_le'  (inode  l s) (inode  l' s').





Lemma t1_le_t2 : itree_le t1 t2.
 unfold t1, t2.
 constructor.
 auto with zarith.
 intro i; exists (2 * i).
 unfold isingle. 
 constructor.
 auto with zarith.
 exists i;constructor.
Qed.



Lemma t1_le'_t2 :  itree_le' t1 t2.
 unfold t1, t2.
 constructor 2  with (fun i : nat => 2 * i).
 auto with zarith.
 unfold isingle;
 intro i ; constructor 2 with (fun i :nat => i).
 auto with zarith.
 constructor .
Qed.


Require Import List.

Inductive ltree  (A:Set) : Set :=  
          lnode   : A -> list (ltree A) -> ltree A.

Inductive prop : Prop :=
 prop_intro : Prop -> prop.

Check (prop_intro prop).

Inductive ex_Prop  (P : Prop -> Prop) : Prop :=
  exP_intro : forall X : Prop, P X -> ex_Prop P.

Lemma ex_Prop_inhabitant : ex_Prop (fun P => P -> P).
Proof.
  exists (ex_Prop (fun P => P -> P)).
 trivial.
Qed.




(*

Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
      match p with exP_intro X HX => X end).
Error:
Incorrect elimination of "p" in the inductive type  
"ex_Prop", the return type has sort "Type" while it should be 
"Prop"

Elimination of an inductive object of sort "Prop"
is not allowed on a predicate in sort "Type"
because proofs can be eliminated only to build proofs

*)


Inductive  typ : Type := 
  typ_intro : Type -> typ. 

Definition typ_inject: typ.
split. 
exact typ.
(*
Defined.

Error: Universe Inconsistency.
*)
Abort.
(*

Inductive aSet : Set :=
  aSet_intro: Set -> aSet.


User error: Large non-propositional inductive types must be in Type

*)

Inductive ex_Set  (P : Set -> Prop) : Type :=
  exS_intro : forall X : Set, P X -> ex_Set P.


Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop :=
  c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p).

Goal (comes_from_the_left _ _ (or_introl  True I)).
split.
Qed.

Goal ~(comes_from_the_left _ _ (or_intror True I)).
 red;inversion 1.
 (* discriminate H0.
 *)
Abort.

Reset comes_from_the_left.

(*






 Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
  match H with
         |  or_introl p => True 
         |  or_intror q => False
  end.

Error:
Incorrect elimination of "H" in the inductive type  
"or", the return type has sort "Type" while it should be 
"Prop"

Elimination of an inductive object of sort "Prop"
is not allowed on a predicate in sort "Type"
because proofs can be eliminated only to build proofs

*)

Definition comes_from_the_left_sumbool
            (P Q:Prop)(x:{P}+{Q}): Prop :=
  match x with
         |  left  p => True 
         |  right q => False
  end.



                    
Close Scope Z_scope.





Theorem S_is_not_O : forall n, S n <> 0. 

Definition Is_zero (x:nat):= match x with 
                                     | 0 => True  
                                     | _ => False
                             end.
 Lemma O_is_zero : forall m, m = 0 -> Is_zero m.
 Proof.
  intros m H; subst m.
  (*  
  ============================
   Is_zero 0
  *)
  simpl;trivial.
 Qed.
 
 red; intros n Hn.
 apply O_is_zero with (m := S n).
 assumption.
Qed.

Theorem disc2 : forall n, S (S n) <> 1. 
Proof.
 intros n Hn; discriminate.
Qed.


Theorem disc3 : forall n, S (S n) = 0 -> forall Q:Prop, Q.
Proof.
  intros n Hn Q.
  discriminate.
Qed.



Theorem inj_succ  : forall n m, S n = S m -> n = m.
Proof.
 

Lemma inj_pred : forall n m, n = m -> pred n = pred m.
Proof.
 intros n m eq_n_m.
 rewrite eq_n_m.
 trivial.
Qed.

 intros n m eq_Sn_Sm.
 apply inj_pred with (n:= S n) (m := S m); assumption.
Qed.

Lemma list_inject : forall (A:Type)(a b :A)(l l':list A),
                     a :: b :: l = b :: a :: l' -> a = b /\ l = l'.
Proof.
 intros A a b l l' e.
 injection e.
 auto.
Qed.


Theorem not_le_Sn_0 : forall n:nat, ~ (S n <= 0).
Proof.
 red; intros n H.
 case H.
Undo.

Lemma not_le_Sn_0_with_constraints :
  forall n p , S n <= p ->  p = 0 -> False.
Proof.
 intros n p H; case H ;
   intros; discriminate.
Qed.
   
eapply not_le_Sn_0_with_constraints; eauto.
Qed. 


Theorem not_le_Sn_0' : forall n:nat, ~ (S n <= 0).
Proof.
 red; intros n H ; inversion H.
Qed.

Derive Inversion le_Sn_0_inv with (forall n :nat, S n <=  0).
Check le_Sn_0_inv.

Theorem le_Sn_0'' : forall n p : nat, ~ S n <= 0 .
Proof.
 intros n p H; 
 inversion H using le_Sn_0_inv.
Qed.

Derive Inversion_clear le_Sn_0_inv' with (forall n :nat, S n <=  0).
Check le_Sn_0_inv'.


Theorem le_reverse_rules : 
 forall n m:nat, n <= m -> 
                   n = m \/  
                   exists p, n <=  p /\ m = S p.
Proof.
  intros n m H; inversion H.
  left;trivial.
  right; exists m0; split; trivial.
Restart.
  intros n m H; inversion_clear H.
  left;trivial.
  right; exists m0; split; trivial.
Qed.

Inductive ArithExp : Set :=
     Zero : ArithExp 
   | Succ : ArithExp -> ArithExp
   | Plus : ArithExp -> ArithExp -> ArithExp.

Inductive RewriteRel : ArithExp -> ArithExp -> Prop :=
     RewSucc  : forall e1 e2 :ArithExp,
                  RewriteRel e1 e2 -> RewriteRel (Succ e1) (Succ e2) 
  |  RewPlus0 : forall e:ArithExp,
                  RewriteRel (Plus Zero e) e 
  |  RewPlusS : forall e1 e2:ArithExp,
                  RewriteRel e1 e2 ->
                  RewriteRel (Plus (Succ e1) e2) (Succ (Plus e1 e2)).


  
Fixpoint plus (n p:nat) {struct n} : nat :=
  match n with
          | 0 => p
          | S m => S (plus m p)
 end.

Fixpoint plus' (n p:nat) {struct p} : nat :=
    match p with
          | 0 => n
          | S q => S (plus' n q)
    end.

Fixpoint plus'' (n p:nat) {struct n} : nat :=
  match n with
          | 0 => p
          | S m => plus'' m (S p)
 end.


Fixpoint even_test (n:nat) : bool :=
  match n 
  with 0 =>  true
     | 1 =>  false
     | S (S p) => even_test p
  end.


Reset even_test.

Fixpoint even_test (n:nat) : bool :=
  match n 
  with 
      | 0 =>  true
      | S p => odd_test p
  end
with odd_test (n:nat) : bool :=
  match n
  with 
     | 0 => false
     | S p => even_test p
 end.


  
Eval simpl in even_test.



Eval simpl in (fun x : nat => even_test x).

Eval simpl in (fun x : nat => plus 5 x).
Eval simpl in (fun x : nat => even_test (plus 5 x)).

Eval simpl in (fun x : nat => even_test (plus x 5)).


Section Principle_of_Induction.
Variable    P               : nat -> Prop.
Hypothesis  base_case       : P 0.
Hypothesis  inductive_step   : forall n:nat, P n -> P (S n).
Fixpoint nat_ind  (n:nat)    : (P n) := 
   match n return P n with
          | 0 => base_case
          | S m => inductive_step m (nat_ind m)
   end. 

End Principle_of_Induction.

Scheme Even_induction := Minimality for even Sort Prop
with   Odd_induction  := Minimality for odd  Sort Prop.

Theorem even_plus_four : forall n:nat, even n -> even (4+n).
Proof.
 intros n H.
 elim H using Even_induction with (P0 := fun n => odd (4+n));
 simpl;repeat constructor;assumption.
Qed.


Section Principle_of_Double_Induction.
Variable    P               : nat -> nat ->Prop.
Hypothesis  base_case1      : forall x:nat, P 0 x.
Hypothesis  base_case2      : forall x:nat, P (S x) 0.
Hypothesis  inductive_step   : forall n m:nat, P n m -> P (S n) (S m).
Fixpoint nat_double_ind (n m:nat){struct n} : P n m := 
  match n, m return P n m with 
         |  0 ,     x    =>  base_case1 x 
         |  (S x),    0  =>  base_case2 x
         |  (S x), (S y) =>  inductive_step x y (nat_double_ind x y)
     end.
End Principle_of_Double_Induction.

Section Principle_of_Double_Recursion.
Variable    P               : nat -> nat -> Type.
Hypothesis  base_case1      : forall x:nat, P 0 x.
Hypothesis  base_case2      : forall x:nat, P (S x) 0.
Hypothesis  inductive_step   : forall n m:nat, P n m -> P (S n) (S m).
Fixpoint nat_double_rect (n m:nat){struct n} : P n m := 
  match n, m return P n m with 
         |   0 ,     x    =>  base_case1 x 
         |  (S x),    0   => base_case2 x
         |  (S x), (S y)  => inductive_step x y (nat_double_rect x y)
     end.
End Principle_of_Double_Recursion.

Definition min : nat -> nat -> nat  := 
  nat_double_rect (fun (x y:nat) => nat)
                 (fun (x:nat) => 0)
                 (fun (y:nat) => 0)
                 (fun (x y r:nat) => S r).

Eval compute in (min 5 8).
Eval compute in (min 8 5).



Lemma not_circular : forall n:nat, n <> S n.
Proof.
 intro n.
 apply nat_ind with (P:= fun n => n <> S n).
 discriminate.
 red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial.
Qed.

Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}.
Proof.
 intros n p.
 apply nat_double_rect with (P:= fun (n q:nat) => {q=p}+{q <> p}).
Undo.
 pattern p,n.
 elim n using nat_double_rect.
 destruct x; auto.
 destruct x; auto.
 intros n0 m H; case H.
 intro eq; rewrite eq ; auto.
 intro neg; right; red ; injection 1; auto.
Defined.

Definition eq_nat_dec' : forall n p:nat, {n=p}+{n <> p}.
 decide equality.
Defined.


Require Import Minus.

(*
Fixpoint div (x y:nat){struct x}: nat :=
 if eq_nat_dec x 0 
  then 0
  else if eq_nat_dec y 0
       then x
       else S (div (x-y) y).

Error:
Recursive definition of div is ill-formed.
In environment
div : nat -> nat -> nat
x : nat
y : nat
_ : x <> 0
_ : y <> 0

Recursive call to div has principal argument equal to
"x - y"
instead of a subterm of x

*)

Lemma minus_smaller_S: forall x y:nat, x - y < S x.
Proof.
 intros x y; pattern y, x;
 elim x using nat_double_ind.
 destruct x0; auto with arith.
 simpl; auto with arith.
 simpl; auto with arith.
Qed.

Lemma minus_smaller_positive : forall x y:nat, x <>0 -> y <> 0 ->
                                     x - y < x.
Proof.
 destruct x; destruct y; 
 ( simpl;intros; apply minus_smaller_S || 
   intros; absurd (0=0); auto).
Qed.

Definition minus_decrease : forall x y:nat, Acc lt x -> 
                                         x <> 0 -> 
                                         y <> 0 ->
                                         Acc lt (x-y).
Proof.
 intros x y H; case H.
 intros Hz posz posy. 
 apply Hz; apply minus_smaller_positive; assumption.
Defined.

Print minus_decrease.



Definition div_aux (x y:nat)(H: Acc lt x):nat.
 fix 3.
 intros.
  refine (if eq_nat_dec x 0 
         then 0 
         else if eq_nat_dec y 0 
              then y
              else div_aux (x-y) y _).
 apply (minus_decrease x y H);assumption. 
Defined.


Print div_aux.
(*
div_aux = 
(fix div_aux (x y : nat) (H : Acc lt x) {struct H} : nat :=
   match eq_nat_dec x 0 with
   | left _ => 0
   | right _ =>
       match eq_nat_dec y 0 with
       | left _ => y
       | right _0 => div_aux (x - y) y (minus_decrease x y H _ _0)
       end
   end)
     : forall x : nat, nat -> Acc lt x -> nat
*)

Require Import Wf_nat.
Definition div x y := div_aux x y (lt_wf x). 

Extraction div.
(*
let div x y =
  div_aux x y
*)

Extraction div_aux.

(*
let rec div_aux x y =
  match eq_nat_dec x O with
    | Left -> O
    | Right ->
        (match eq_nat_dec y O with
           | Left -> y
           | Right -> div_aux (minus x y) y)
*)

Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
Proof.
 intros A v;inversion v.
Abort.

(*
 Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n), 
                                  n= 0 -> v = Vnil A.

Toplevel input, characters 40281-40287
> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),                                    n= 0 -> v = Vnil A.
>                                                                                                                 ^^^^^^
Error: In environment
A : Set
n : nat
v : vector A n
e : n = 0
The term "Vnil A" has type "vector A 0" while it is expected to have type
 "vector A n"
*)
 Require Import JMeq.


(* On devrait changer Set en Type ? *)

Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n), 
                                  n= 0 -> JMeq v (Vnil A).
Proof.
 destruct v.
 auto.
 intro; discriminate.
Qed.

Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
Proof.
 intros a v;apply JMeq_eq.
 apply vector0_is_vnil_aux.
 trivial.
Qed.


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

Definition Vid : forall (A : Type)(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:Type)(v:vector A 0) => (Vid _ _ v)).

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



Lemma Vid_eq : forall (n:nat) (A:Type)(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 : Type) (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:Type) (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:Type)(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.

 Set Implicit Arguments.

 CoInductive Stream (A:Type) : Type   :=
 |  Cons : A -> Stream A -> Stream A.

 CoInductive LList (A: Type) : Type :=
 |  LNil : LList A
 |  LCons : A -> LList A -> LList A.


 


 Definition head (A:Type)(s : Stream A) := match s with Cons a s' => a end.

 Definition tail (A : Type)(s : Stream A) :=
      match s with Cons a s' => s' end.

 CoFixpoint repeat (A:Type)(a:A) : Stream A := Cons a (repeat a).

 CoFixpoint iterate (A: Type)(f: A -> A)(a : A) : Stream A:=
    Cons a (iterate f (f a)).

 CoFixpoint map (A B:Type)(f: A -> B)(s : Stream A) : Stream B:=
  match s with Cons a tl => Cons (f a) (map f tl) end.

Eval simpl in (fun (A:Type)(a:A) => repeat a).

Eval simpl in (fun (A:Type)(a:A) => head (repeat a)).


CoInductive EqSt (A: Type) : Stream A -> Stream A -> Prop :=
  eqst : forall s1 s2: Stream A,
      head s1 = head s2 ->
      EqSt (tail s1) (tail s2) ->
      EqSt s1 s2.


Section Parks_Principle.
Variable A : Type.
Variable    R      : Stream A -> Stream A -> Prop.
Hypothesis  bisim1 : forall s1 s2:Stream A, R s1 s2 ->
                                          head s1 = head s2.
Hypothesis  bisim2 : forall s1 s2:Stream A, R s1 s2 ->
                                          R (tail s1) (tail s2).

CoFixpoint park_ppl     : forall s1 s2:Stream A, R s1 s2 ->
                                               EqSt s1 s2 :=
 fun s1 s2 (p : R s1 s2) =>
      eqst s1 s2 (bisim1  p) 
                 (park_ppl  (bisim2  p)).
End Parks_Principle.


Theorem map_iterate : forall (A:Type)(f:A->A)(x:A),
                       EqSt (iterate f (f x)) (map f (iterate f x)).
Proof.
 intros A f x.
 apply park_ppl with
   (R:=  fun s1 s2 => exists x: A, 
                      s1 = iterate f (f x) /\ s2 = map f (iterate f x)).

 intros s1 s2 (x0,(eqs1,eqs2));rewrite eqs1;rewrite eqs2;reflexivity.
 intros s1 s2 (x0,(eqs1,eqs2)).
 exists (f x0);split;[rewrite eqs1|rewrite eqs2]; reflexivity.
 exists x;split; reflexivity.
Qed.

Ltac infiniteproof f :=
  cofix f; constructor; [clear f| simpl; try (apply f; clear f)].


Theorem map_iterate' : forall (A:Type)(f:A->A)(x:A),
                       EqSt (iterate f (f x)) (map f (iterate f x)).
infiniteproof map_iterate'.
 reflexivity.
Qed.


Implicit Arguments LNil [A].

Lemma Lnil_not_Lcons : forall (A:Type)(a:A)(l:LList A),
                               LNil <> (LCons a l).
 intros;discriminate.
Qed.

Lemma injection_demo : forall (A:Type)(a b : A)(l l': LList A),
                       LCons a (LCons b l) = LCons b (LCons a l') ->
                       a = b /\ l = l'.
Proof.
 intros A a b l l' e; injection e; auto.
Qed.


Inductive Finite (A:Type) : LList A -> Prop :=
|  Lnil_fin : Finite (LNil (A:=A))
|  Lcons_fin : forall a l, Finite l -> Finite (LCons a l).

CoInductive Infinite  (A:Type) : LList A -> Prop :=
| LCons_inf : forall a l, Infinite l -> Infinite (LCons a l).

Lemma LNil_not_Infinite : forall (A:Type), ~ Infinite (LNil (A:=A)).
Proof.
  intros A H;inversion H.
Qed.

Lemma Finite_not_Infinite : forall (A:Type)(l:LList A),
                                Finite l -> ~ Infinite l.
Proof.
 intros A l H; elim H.
 apply LNil_not_Infinite.
 intros a l0 F0 I0' I1.
 case I0'; inversion_clear I1.
 trivial.
Qed.

Lemma Not_Finite_Infinite : forall (A:Type)(l:LList A),
                            ~ Finite l -> Infinite l.
Proof.
 cofix H.
 destruct l.
 intro; absurd (Finite (LNil (A:=A)));[auto|constructor].
 constructor.
 apply H.
 red; intro H1;case H0.
 constructor.
 trivial.
Qed.




check.patch:

--- NEW FILE check.patch ---
--- test-suite/check	2008-06-17 09:18:42.000000000 -0400
+++ test-suite/check	2008-06-17 09:19:11.000000000 -0400
@@ -52,7 +52,7 @@
 	nbtests=`expr $nbtests + 1`
 	printf "    "$f"..."
         tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
-	$command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" > $tmpoutput
+	$command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" | grep -v "some rule has been masked" > $tmpoutput
         foutput=`dirname $f`/`basename $f .v`.out
         diff $tmpoutput $foutput >& /dev/null
 	if [ $? = 0 ]; then 

cmxa-install.patch:

--- NEW FILE cmxa-install.patch ---
--- Makefile	2007-11-12 10:10:25.000000000 -0500
+++ Makefile	2008-06-16 10:58:38.000000000 -0400
@@ -1271,7 +1271,12 @@
         parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
         parsing/highparsing.cma tactics/hightactics.cma contrib/contrib.cma
 
-OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
+ifeq ($(BEST),opt)
+  OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
+else
+  OBJECTCMXA=
+endif
+
 
 install-library:
 	$(MKDIR) $(FULLCOQLIB)


--- NEW FILE coq.spec ---
# Upstream includes option for generation of optimized binaries,
# however, specifically generates bytecode versions for certain
# executables even when optimized option is set, namely the following:

# coq-tex, coq_makefile, coq-interface, coqwc, coqdoc, parser, coqdep,
# gallina

# (coqtop.byte, coqide.byte binaries are also made available.)

# .coqide-gtk2rc also produces an rpmlint warning due to its name,
# however, this name is proper as per the Coq documentation

# Disable creation of the debug package: if bytecode executables are
# created find-debuginfo.sh will ruin them, while if optimized
# executables are created they will be stripped by the Makefile
# anyway, thus we won't get anything useful from the debug info
# package creation.
#
# It appears as though ALL of these are necessary to prevent unwanted
# stripping
%define __os_install_post /usr/lib/rpm/brp-compress %{nil}
%define _enable_debug_package 0
%define debug_package %{nil}

Name:		coq
Version:	8.1pl3
Release:	1%{?dist}
Summary:	Coq proof management system

Group:		Applications/Engineering
License:	LGPLv2
URL:		http://coq.inria.fr/
Source0:	http://coq.inria.fr/V%{version}/files/coq-%{version}.tar.gz
Source1:	Coq-Library.pdf.gz
Source2:	Coq-Reference-Manual.pdf.gz
Source3:	Coq-Tutorial.v.pdf.gz 
Source4:	Coq-RecTutorial.pdf.gz
Source5:	coq-refman-html.tar.gz
Source6:	coq-stdlib-html.tar.gz
Source7:	RecTutorial.v
Source8:	coqide.desktop
Source9:	coq-icon.png
Source10:	README.coq-emacs
Patch0:		makefile.patch
Patch1:		cmxa-install.patch
Patch2:		makefile-strip.patch
Patch3:		check.patch
BuildRoot:	%{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
BuildRequires:	ocaml >= 3.08, ocaml-camlp5-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, emacs, texlive-latex, texlive-texmf
# ExcludeArch:	ppc64

%description
Coq is a formal proof management system. It allows for the development
of theorems through first order logic that are mechanically checked by
the machine. Sets of definitions and theorems can be saved as compiled
modules and loaded into the system.

This package provides the main Coq binary without an optional IDE,
Coqide.

# The IDE's package name will become "coq-coqide".  That way,
# searching for either "coqide" (the Ubuntu/Debian package name, and
# also the full name of the IDE) or "coq" and "ide" will find
# this. (If the package were named "coq-ide", the former would fail.)
%package coqide
Group:		Applications/Engineering
Summary:	Coqide IDE for Coq proof management system
Requires:	coq

%description coqide
Coq is a formal proof management system. It allows for the development
of theorems through first order logic that are mechanically checked by
the machine. Sets of definitions and theorems can be saved as compiled
modules and loaded into the system.

This package provides Coqide, a lightweight IDE for Coq.

%package doc
Group:		Applications/Engineering
Summary:	Documentation for Coq proof management system

%description doc
Coq is a formal proof management system. It allows for the development
of theorems through first order logic that are mechanically checked by
the machine. Sets of definitions and theorems can be saved as compiled
modules and loaded into the system.

This package provides documentation and tutorials for the system. The
main documentation comes in two parts: the main Library documentation,
which decribes all Coq.* modules, and the Reference Manual, which
gives a more complete description of the whole system. Included are
also HTML versions of both. Furthermore, there are two tutorials, the
main one, and one specifically on recursive types. The example code
for the latter is also included.

%package emacs
Group:		Applications/Engineering
Summary:	Elisp files for Coq proof management system
Requires:	coq, emacs

%description emacs
Coq is a formal proof management system. It allows for the development
of theorems through first order logic that are mechanically checked by
the machine. Sets of definitions and theorems can be saved as compiled
modules and loaded into the system.

This package provides emacs mode files for formatting Coq input.

%prep
%setup -q

# Patch description:
# Considered each of the seven patches from the Debian Coq package:

# Credit goes to the Debian patch creators for their patches
# (See http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/trunk/debian/patches/?rev=0&sc=0)
#
# For most patches I merely reproduced the results in non-dpatch
# form. I opted for no patching in cases where it did not seem
# necessary or immediately correct.
#

# - browser.dpatch: changes firefox option for linux, however, link
# x-www-browser does not exist in Fedora setup, and changing this
# option does not actually fix the problem in the IDE wherein a
# browser window needs to be open in order to actually open any help
# file -> do not change until the real source of the problem can be
# detected
# - check.dpatch: suppress a test warning, similar change made in my
# check.patch
# - cmxa-install.dpatch: fixes cmxa install by testing for opt, similar
# change made in cmxa-install.patch
# - configure.dpatch: fixes detection of ocamlopt - We do this detection
# seperately anyway in this RPM, no change made
# - coqdoc_stdlib.dpatch: extra documentation option - Perhaps do this
# in the future, but for now, no change made
# - makefile.dpatch: fix testing on non-native architecture compiles, similar change made in makefile.patch
# - no-complexity-test.dpatch: turn off some of the tests - Perhaps this
# change was made due to a failure in complexity tests when they
# "don't run quickly enough", which is likely to be incredibly
# variable, but unsure, so no change made

%patch0
%patch1

# I created patch3 to consistently strip native-code binaries, unlike
# the inconsistent way it was done in the original makefile
%patch2

# This patch may not be strictly necessary unless the tests are
# incorporated into the build process somehow. However, the tests don't
# work properly without it.
%patch3

# Fix some files that are not in UTF-8 encoding

for f in CHANGES CREDITS COPYRIGHT; do
mv $f $f.old; iconv -f ISO-8859-1 -t UTF-8 < $f.old > $f; rm $f.old
done

%define emacs_lispdir %{_datadir}/emacs/site-lisp
%define tex_dir %{_datadir}/texmf/tex/latex/misc

# Seems like setup only sets up the main file
cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 %SOURCE10 .
gunzip *.gz
for f in *.tar; do
tar xf $f
done

%build
%define opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)

# optimized binary ppc64 building does not work at the moment - the
# log files are no real help, but we fail on bootstrap with the
# optimized compiler:
#
# bin/coqtop.opt -boot -nois -compile theories/Init/Notations
#
# appears to be the command that dies. It appears that the status of
# OCaml has been somewhat uncertain on ppc64, perhaps this is the cause?
# However, bytecode compilation DOES work -> do this for now
%ifarch ppc64
%define opt 0
%endif

# Define opt flag based upon prior opt detection and restrictions
%if %{opt}
%define opt_option --opt
%else
%define opt_option --byte-only
%endif

bash configure -prefix %{_prefix} -libdir %{_datadir}/coq -bindir %{_bindir} -mandir %{_mandir} -emacs %{emacs_lispdir} -coqdocdir %{tex_dir} %{opt_option} -reals all > /dev/null
make world 2>/dev/null

# Fix permissions in the documentation
chmod -R a+rX refman stdlib

%install
rm -rf %{buildroot}

make COQINSTALLPREFIX="%{buildroot}" install

# Install desktop icon and menu entry

%define coqdatadir %{_datadir}/coq
%if %(test -d %{buildroot}%{coqdatadir} && echo 1 || echo 0) != 1
mkdir -p %{buildroot}%{coqdatadir}
%endif
cp coq-icon.png %{buildroot}%{coqdatadir}

sed -i -e 's|ICON-LOCATION-BASE|%{coqdatadir}|' coqide.desktop

desktop-file-install --vendor="fedora"			\
--dir=%{buildroot}%{_datadir}/applications		\
coqide.desktop

# Install tutorial code

%define tutorialcodedir %{coqdatadir}/tutorial
%if %(test -d %{buildroot}%{tutorialcodedir} && echo 1 || echo 0) != 1
mkdir -p %{buildroot}%{tutorialcodedir}
%endif
mv RecTutorial.v %{buildroot}%{tutorialcodedir}

%clean
rm -rf %{buildroot}

# Note: we want to keep both coqtop.opt and coqtop.byte because the
# byte compiled version can be used to compile new version through
# coqmktop

%files
%defattr(-,root,root,-)
%doc CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL KNOWN-BUGS LICENSE README
%doc %{_mandir}/man1/coq*
%doc %{_mandir}/man1/gallina.1.gz
%doc %{_mandir}/man1/parser.1.gz
%{_datadir}/coq
%{_bindir}/coq*
%{_bindir}/gallina
%{_bindir}/parser
%if %{opt}
%{_bindir}/parser.opt
%endif
# Exclude ide files to put in a separate package
%exclude %{_bindir}/coqide*
%exclude %{_datadir}/coq/ide
%if %{opt}
%exclude %{_datadir}/coq/*.cmxa
%endif
%{tex_dir}/coq*

%files coqide
%defattr(-,root,root,-)
%doc INSTALL.ide
%{_bindir}/coqide*
%{_datadir}/coq/ide
# Exclude a corrupted file from the tarball
%exclude %{_datadir}/coq/ide/coq.png
# Instead include a non-corrupted icon somewhere else
%dir %{coqdatadir}
%{coqdatadir}/coq-icon.png

# Is it ok to assume this is what desktop-file-install renames coqide.desktop to?
%{_datadir}/applications/fedora-coqide.desktop

%files doc
%defattr(-,root,root,-)
%doc Coq-Library.pdf
%doc Coq-Reference-Manual.pdf
%doc Coq-Tutorial.v.pdf
%doc Coq-RecTutorial.pdf
%dir %{coqdatadir}
%{tutorialcodedir}
# Standard permissions with - in defattr make the manual unreadable... unknown how to fix
%doc refman
%doc stdlib

%files emacs
%defattr(-,root,root,-)
%{_datadir}/emacs/site-lisp/coq*
%doc README.coq-emacs

%changelog
* Wed Jun 14 2008 Alan Dunn <amdunn at gmail.com> 8.1pl3-1
- Initial Fedora RPM version.


--- NEW FILE coqide.desktop ---
[Desktop Entry]
Encoding=UTF-8
Name=CoqIDE
Comment=Examine and develop Coq .v files
Exec=coqide
Icon=ICON-LOCATION-BASE/coq-icon.png
Type=Application
Categories=Development;

--- NEW FILE import.log ---
coq-8_1pl3-1_fc9:HEAD:coq-8.1pl3-1.fc9.src.rpm:1216233878

makefile-strip.patch:

--- NEW FILE makefile-strip.patch ---
--- Makefile	2007-11-12 10:10:25.000000000 -0500
+++ Makefile	2008-06-17 00:43:48.000000000 -0400
@@ -431,6 +431,7 @@
 	$(SHOW)'OCAMLOPT -o $@'	
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa \
           $(COQMKTOPCMX) $(OSDEPLIBS)
+	$(STRIP) $@
 
 $(COQMKTOP): $(BESTCOQMKTOP)
 	cd bin; ln -sf coqmktop.$(BEST)$(EXE) coqmktop$(EXE)
@@ -457,6 +458,7 @@
 $(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ unix.cmxa $(COQCCMX) $(OSDEPLIBS)
+	$(STRIP) $@
 
 $(COQC): $(BESTCOQC)
 	cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE)
@@ -746,6 +748,7 @@
 bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(USERTACCMX) $(INTERFACECMX)
 	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(INTERFACECMX)
+	$(STRIP) $@
 
 PARSERCODE=contrib/interface/line_parser.cmo contrib/interface/vtp.cmo \
            contrib/interface/xlate.cmo contrib/interface/parse.cmo
@@ -761,6 +764,7 @@
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \
 	  $(LIBCOQRUN) $(CMXA) $(PARSERCMX)
+	$(STRIP) $@
 
 INTERFACEVO=
 

makefile.patch:

--- NEW FILE makefile.patch ---
--- Makefile	2007-11-12 10:10:25.000000000 -0500
+++ Makefile	2008-06-16 09:48:05.000000000 -0400
@@ -1481,7 +1481,7 @@
 parsing/grammar.cma: $(GRAMMARCMO)
 	$(SHOW)'Testing $@'
 	@touch test.ml4
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
+	$(HIDE)$(OCAMLC) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
 	@rm -f test-grammar test.*
 	$(SHOW)'OCAMLC -a $@'   
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@


Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/coq/devel/.cvsignore,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- .cvsignore	15 Jul 2008 16:48:21 -0000	1.1
+++ .cvsignore	16 Jul 2008 18:49:27 -0000	1.2
@@ -0,0 +1,7 @@
+Coq-Library.pdf.gz
+Coq-RecTutorial.pdf.gz
+Coq-Reference-Manual.pdf.gz
+Coq-Tutorial.v.pdf.gz
+coq-8.1pl3.tar.gz
+coq-refman-html.tar.gz
+coq-stdlib-html.tar.gz


Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/coq/devel/sources,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- sources	15 Jul 2008 16:48:21 -0000	1.1
+++ sources	16 Jul 2008 18:49:27 -0000	1.2
@@ -0,0 +1,7 @@
+8b14a9c8f65ea5bd592901b3649346a7  Coq-Library.pdf.gz
+0e3d5eac23416ec75dd59fabdcc1367c  Coq-RecTutorial.pdf.gz
+021c58a1f2e5d029928ffae0cc9703b0  Coq-Reference-Manual.pdf.gz
+bcb4d1c4857bfdae5c22f8fc0be6853c  Coq-Tutorial.v.pdf.gz
+84311faf7865b2eab964990cdb365dca  coq-8.1pl3.tar.gz
+04285e3a76571db6e1d2fbe198c76120  coq-refman-html.tar.gz
+17b1edf9122fd89c8b99d4e047b54fb8  coq-stdlib-html.tar.gz