Move Program tactics into a proper theories/ directory as they are general purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 514 insertions, 0 deletions

diff --git a/theories/Program/FixSub.v b/theories/Program/FixSub.v
new file mode 100644
index 0000000000..58ac9d90ee
--- /dev/null
+++ b/theories/Program/FixSub.v
@@ -0,0 +1,148 @@
+Require Import Wf.
+Require Import Coq.Program.Utils.
+Require Import ProofIrrelevance.
+
+(** Reformulation of the Wellfounded module using subsets where possible. *)
+
+Section Well_founded.
+  Variable A : Type.
+  Variable R : A -> A -> Prop.
+  Hypothesis Rwf : well_founded R.
+  
+  Section Acc.
+    
+    Variable P : A -> Type.
+    
+    Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
+    
+    Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
+      F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y) 
+        (Acc_inv r (proj1_sig y) (proj2_sig y))).
+    
+    Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
+  End Acc.
+  
+  Section FixPoint.
+    Variable P : A -> Type.
+    
+    Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
+    
+    Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *)
+    
+    Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x).
+    
+    Hypothesis
+      F_ext :
+      forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
+        (forall y:{ y:A | R y x}, f y = g y) -> F_sub x f = F_sub x g.
+
+    Lemma Fix_F_eq :
+      forall (x:A) (r:Acc R x),
+        F_sub x (fun (y:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r.
+    Proof. 
+      destruct r using Acc_inv_dep; auto.
+    Qed.
+    
+    Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s.
+    Proof.
+      intro x; induction (Rwf x); intros.
+      rewrite <- (Fix_F_eq x r); rewrite <- (Fix_F_eq x s); intros.
+      apply F_ext; auto.
+      intros.
+      rewrite (proof_irrelevance (Acc R x) r s) ; auto.
+    Qed.
+
+    Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{y:A|R y x}) => Fix (proj1_sig y)).
+    Proof.
+      intro x; unfold Fix in |- *.
+      rewrite <- (Fix_F_eq ).
+      apply F_ext; intros.
+      apply Fix_F_inv.
+    Qed.
+
+    Lemma fix_sub_eq :
+        forall x : A,
+          Fix_sub P F_sub x =
+          let f_sub := F_sub in
+            f_sub x (fun  {y : A | R y x}=> Fix (`y)).
+      exact Fix_eq.
+    Qed.
+
+ End FixPoint.
+
+End Well_founded.
+
+Extraction Inline Fix_F_sub Fix_sub.
+
+Require Import Wf_nat.
+Require Import Lt.
+
+Section Well_founded_measure.
+  Variable A : Type.
+  Variable m : A -> nat.
+  
+  Section Acc.
+    
+    Variable P : A -> Type.
+    
+    Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
+    
+    Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
+      F_sub x (fun y: { y : A | m y < m x}  => Fix_measure_F_sub (proj1_sig y) 
+        (Acc_inv r (m (proj1_sig y)) (proj2_sig y))).
+    
+    Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
+  
+  End Acc.
+
+  Section FixPoint.
+    Variable P : A -> Type.
+    
+    Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
+    
+    Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *)
+    
+    Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)).
+    
+    Hypothesis
+      F_ext :
+      forall (x:A) (f g:forall y:{y:A | m y < m x}, P (`y)),
+        (forall y:{ y:A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
+
+    Lemma Fix_measure_F_eq :
+      forall (x:A) (r:Acc lt (m x)),
+        F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (proj2_sig y))) = Fix_F x r.
+    Proof.
+      intros x.
+      set (y := m x).
+      unfold Fix_measure_F_sub.
+      intros r ; case r ; auto.
+    Qed.
+    
+    Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s.
+    Proof.
+      intros x r s.
+      rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto.
+    Qed.
+
+    Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)).
+    Proof.
+      intro x; unfold Fix_measure in |- *.
+      rewrite <- (Fix_measure_F_eq ).
+      apply F_ext; intros.
+      apply Fix_measure_F_inv.
+    Qed.
+
+    Lemma fix_measure_sub_eq :
+        forall x : A,
+          Fix_measure_sub P F_sub x =
+          let f_sub := F_sub in
+            f_sub x (fun  {y : A | m y < m x}=> Fix_measure (`y)).
+      exact Fix_measure_eq.
+    Qed.
+
+ End FixPoint.
+
+End Well_founded_measure.
+
+Extraction Inline Fix_measure_F_sub Fix_measure_sub.
diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
new file mode 100644
index 0000000000..c6e5a64fb3
--- /dev/null
+++ b/theories/Program/FunctionalExtensionality.v
@@ -0,0 +1,65 @@
+Require Import Coq.Program.Utils.
+Require Import Coq.Program.FixSub.
+
+(** The converse of functional equality. *)
+
+Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
+  f = g -> forall x, f x = g x.
+Proof.
+  intros.
+  rewrite H.
+  auto.
+Qed.
+
+(** Statements of functional equality for simple and dependent functions. *)
+
+Axiom fun_extensionality : forall A B (f g : A -> B), 
+  (forall x, f x = g x) -> f = g.
+
+Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), forall (f g : forall x : A, B x), 
+  (forall x, f x = g x) -> f = g.
+
+Hint Resolve fun_extensionality fun_extensionality_dep : program.
+
+(** The two following lemmas allow to unfold a well-founded fixpoint definition without
+   restriction using the functional extensionality axiom. *)
+
+(** For a function defined with Program using a well-founded order. *)
+
+Lemma fix_sub_eq_ext :
+  forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
+    (P : A -> Set)
+    (F_sub : forall x : A, (forall  {y : A | R y x}, P (`y)) -> P x),
+    forall x : A,
+      Fix_sub A R Rwf P F_sub x =
+        F_sub x (fun {y : A | R y x}=> Fix A R Rwf P F_sub (`y)).
+Proof.
+  intros ; apply Fix_eq ; auto.
+  intros.
+  assert(f = g).
+  apply (fun_extensionality_dep _ _ _ _ H).
+  rewrite H0 ; auto.
+Qed.
+
+(** For a function defined with Program using a measure. *)
+
+Lemma fix_sub_measure_eq_ext :
+  forall (A : Type) (f : A -> nat) (P : A -> Type)
+    (F_sub : forall x : A, (forall  {y : A | f y < f x}, P (`y)) -> P x),
+    forall x : A,
+      Fix_measure_sub A f P F_sub x =
+        F_sub x (fun {y : A | f y < f x}=> Fix_measure_sub A f P F_sub (`y)).
+Proof.
+  intros ; apply Fix_measure_eq ; auto.
+  intros.
+  assert(f0 = g).
+  apply (fun_extensionality_dep _ _ _ _ H).
+  rewrite H0 ; auto.
+Qed.
+
+Ltac apply_ext :=
+  match goal with 
+    [ |- ?x = ?y ] => apply (@fun_extensionality _ _ x y)
+  end.
+
+
diff --git a/theories/Program/Heq.v b/theories/Program/Heq.v
new file mode 100644
index 0000000000..cd405219f6
--- /dev/null
+++ b/theories/Program/Heq.v
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Permut.v 9245 2006-10-17 12:53:34Z notin $ i*)
+
+(** Tactics related to (dependent) equality and proof irrelevance. *)
+
+Require Export ProofIrrelevance.
+Require Export JMeq.
+
+(** Notation for heterogenous equality. *)
+
+Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level).
+
+(** Do something on an heterogeneous equality appearing in the context. *)
+
+Ltac on_JMeq tac := 
+  match goal with
+    | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H
+  end.
+
+(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *)
+
+Ltac simpl_one_JMeq :=
+  on_JMeq 
+  ltac:(fun H => let H' := fresh "H" in 
+    assert (H' := JMeq_eq H) ; clear H ; rename H' into H).
+
+(** Repeat it for every possible hypothesis. *)
+
+Ltac simpl_JMeq := repeat simpl_one_JMeq.
+
+(** Just simplify an h.eq. without clearing it. *)
+
+Ltac simpl_one_dep_JMeq :=
+  on_JMeq
+  ltac:(fun H => let H' := fresh "H" in 
+    assert (H' := JMeq_eq H)).
+
+Require Import Eqdep.
+
+(** Tries to eliminate a call to [eq_rect] (the substitution principle) by any means available. *)
+
+Ltac elim_eq_rect :=
+  match goal with
+    | [ |- ?t ] => 
+      match t with
+        | context [ @eq_rect _ _ _ _ _ ?p ] => 
+          let P := fresh "P" in 
+            set (P := p); simpl in P ; 
+	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
+        | context [ @eq_rect _ _ _ _ _ ?p _ ] => 
+          let P := fresh "P" in 
+            set (P := p); simpl in P ; 
+	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
+      end
+  end.
+
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
new file mode 100644
index 0000000000..4dc50694fa
--- /dev/null
+++ b/theories/Program/Program.v
@@ -0,0 +1,3 @@
+Require Export Coq.Program.Utils.
+Require Export Coq.Program.FixSub.
+Require Export Coq.Program.Heq.
\ No newline at end of file
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
new file mode 100644
index 0000000000..d5ccdf1c5b
--- /dev/null
+++ b/theories/Program/Tactics.v
@@ -0,0 +1,165 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(** This module implements various tactics used to simplify the goals produced by Program. *)
+
+(** Destructs one pair, without care regarding naming. *)
+
+Ltac destruct_one_pair :=
+ match goal with
+   | [H : (_ /\ _) |- _] => destruct H
+   | [H : prod _ _ |- _] => destruct H
+ end.
+
+(** Repeateadly destruct pairs. *)
+
+Ltac destruct_pairs := repeat (destruct_one_pair).
+
+(** Destruct one existential package, keeping the name of the hypothesis for the first component. *)
+
+Ltac destruct_one_ex :=
+  let tac H := let ph := fresh "H" in destruct H as [H ph] in
+    match goal with
+      | [H : (ex _) |- _] => tac H
+      | [H : (sig ?P) |- _ ] => tac H
+      | [H : (ex2 _) |- _] => tac H
+    end.
+
+(** Repeateadly destruct existentials. *)
+
+Ltac destruct_exists := repeat (destruct_one_ex).
+
+(** Repeateadly destruct conjunctions and existentials. *)
+
+Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex).
+
+(** Destruct an existential hypothesis [t] keeping its name for the first component 
+   and using [Ht] for the second *)
+
+Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht].
+
+(** Destruct a disjunction keeping its name in both subgoals. *)
+
+Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H].
+
+(** Discriminate that also work on a [x <> x] hypothesis. *)
+Ltac discriminates :=
+  match goal with
+    | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity
+    | _ => discriminate
+  end.
+
+(** Revert the last hypothesis. *)
+
+Ltac revert_last := 
+  match goal with
+    [ H : _ |- _ ] => revert H
+  end.
+
+(** Reapeateadly reverse the last hypothesis, putting everything in the goal. *)
+
+Ltac reverse := repeat revert_last.
+
+(** A non-failing subst that substitutes as much as possible. *)
+
+Tactic Notation "subst" "*" :=
+  repeat (match goal with 
+            [ H : ?X = ?Y |- _ ] => subst X || subst Y                  
+          end).
+
+(** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *)
+Ltac on_call f tac :=
+  match goal with
+    | H : ?T |- _  =>
+      match T with
+        | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u)
+        | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v)
+        | context [f ?x ?y ?z ?w] => tac (f x y z w)
+        | context [f ?x ?y ?z] => tac (f x y z)
+        | context [f ?x ?y] => tac (f x y) 
+        | context [f ?x] => tac (f x)
+      end
+    | |- ?T  =>
+      match T with
+        | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u)
+        | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v)
+        | context [f ?x ?y ?z ?w] => tac (f x y z w)
+        | context [f ?x ?y ?z] => tac (f x y z)
+        | context [f ?x ?y] => tac (f x y)
+        | context [f ?x] => tac (f x)
+      end
+  end.
+
+(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object. *)
+
+Ltac destruct_call f :=
+  let tac t := destruct t in on_call f tac.
+
+Ltac destruct_call_as f l :=
+  let tac t := destruct t as l in on_call f tac.
+
+Tactic Notation "destruct_call" constr(f) := destruct_call f.
+
+(** Permit to name the results of destructing the call to [f]. *)
+
+Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l.
+
+(** Try to inject any potential constructor equality hypothesis. *)
+
+Ltac autoinjection :=
+  let tac H := inversion H ; subst ; clear H in
+    match goal with
+      | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
+      | [ H : ?f ?a ?b = ?f' ?a' ?b'  |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g'  |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H
+    end.
+
+(** Destruct an hypothesis by first copying it to avoid dependencies. *)
+
+Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0.
+
+(** If bang appears in the goal, it means that we have a proof of False and the goal is solved. *)
+
+Ltac bang :=
+  match goal with
+    | |- ?x => 
+      match x with
+        | context [False_rect _ ?p] => elim p
+      end
+  end.
+ 
+(** A tactic to show contradiction by first asserting an automatically provable hypothesis. *)
+Tactic Notation "contradiction" "by" constr(t) := 
+  let H := fresh in assert t as H by auto with * ; contradiction.
+
+(** The following tactics allow to do induction on an already instantiated inductive predicate
+   by first generalizing it and adding the proper equalities to the context, in a manner similar to 
+   the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
+
+Tactic Notation "dependent" "induction" ident(H) := 
+  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
+    induction H ; intros ; subst* ; try discriminates.
+
+(** This tactic also generalizes the goal by the given variables before the induction. *)
+
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
+  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
+    generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates.
+
+(** The default simplification tactic used by Program. *)
+
+Ltac program_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; 
+  try (solve [ red ; intros ; discriminate ]) ; auto with *.  
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
new file mode 100644
index 0000000000..a87eda0a26
--- /dev/null
+++ b/theories/Program/Utils.v
@@ -0,0 +1,70 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Coq.Program.Tactics.
+
+Set Implicit Arguments.
+
+(** Wrap a proposition inside a subset. *)
+
+Notation " {{ x }} " := (tt : { y : unit | x }).
+
+(** A simpler notation for subsets defined on a cartesian product. *)
+
+Notation "{ ( x , y )  :  A  |  P }" := 
+  (sig (fun anonymous : A => let (x,y) := anonymous in P))
+  (x ident, y ident) : type_scope.
+
+(** Generates an obligation to prove False. *)
+
+Notation " ! " := (False_rect _ _).
+
+(** Abbreviation for first projection and hiding of proofs of subset objects. *)
+
+Notation " ` t " := (proj1_sig t) (at level 10) : core_scope.
+Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
+
+(** Coerces objects to their support before comparing them. *)
+
+Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70).
+
+(** Quantifying over subsets. *)
+
+Notation "'fun' { x : A | P } => Q" :=
+  (fun x:{x:A|P} => Q)
+  (at level 200, x ident, right associativity).
+
+Notation "'forall' { x : A | P } , Q" :=
+  (forall x:{x:A|P}, Q)
+  (at level 200, x ident, right associativity).
+
+Require Import Coq.Bool.Sumbool.
+
+(** Construct a dependent disjunction from a boolean. *)
+
+Notation "'dec'" := (sumbool_of_bool) (at level 0). 
+
+(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *)
+
+Notation in_right := (@right _ _ _).
+Notation in_left := (@left _ _ _).
+
+(** Extraction directives *)
+
+Extraction Inline proj1_sig.
+Extract Inductive unit => "unit" [ "()" ].
+Extract Inductive bool => "bool" [ "true" "false" ].
+Extract Inductive sumbool => "bool" [ "true" "false" ].
+(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
+(* Extract Inductive sigT => "prod" [ "" ]. *)
+
+(** The scope in which programs are typed (not their types). *)
+
+Delimit Scope program_scope with prg.