The Coq part of the reflexive tactic is now able to handle also

irreflexive relations (in particular partial setoids, also called
typoids). This feature was asked by Marco Maggesi.

The Coq part of the tactic has now reached the planned expressive power.
However, the ML part does not exploit yet the full expressiveness.


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

1 files changed, 105 insertions, 11 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index d98f94419..91745c98b 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -25,6 +25,8 @@ Inductive X_Relation_Class (X: Type) : Type :=
    SymmetricReflexive :
      forall A Aeq, @is_symmetric A Aeq -> is_reflexive Aeq -> X_Relation_Class X
  | AsymmetricReflexive : X -> forall A Aeq, @is_reflexive A Aeq -> X_Relation_Class X
+ | Symmetric : forall A Aeq, @is_symmetric A Aeq -> X_Relation_Class X
+ | Asymmetric : X -> forall A (Aeq : A -> A -> Prop), X_Relation_Class X
  | Leibniz : Type -> X_Relation_Class X.
 
 Inductive variance : Set :=
@@ -40,6 +42,8 @@ Definition relation_class_of_argument_class : Argument_Class -> Relation_Class.
  destruct 1.
  exact (SymmetricReflexive _ i i0).
  exact (AsymmetricReflexive tt i).
+ exact (Symmetric _ i).
+ exact (Asymmetric tt Aeq).
  exact (Leibniz _ T).
 Defined.
 
@@ -47,6 +51,8 @@ Definition carrier_of_relation_class : forall X, X_Relation_Class X -> Type.
  destruct 1.
  exact A.
  exact A.
+ exact A.
+ exact A.
  exact T.
 Defined.
 
@@ -55,6 +61,8 @@ Definition relation_of_relation_class :
  destruct R.
  exact Aeq.
  exact Aeq.
+ exact Aeq.
+ exact Aeq.
  exact (@eq T).
 Defined.
 
@@ -90,12 +98,20 @@ Definition make_compatibility_goal_aux:
      destruct x.
         exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
         exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f x1) (g x2)).
+      exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
+      destruct x.
+        exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
+        exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f x1) (g x2)).
       exact (forall x, relation_of_relation_class Out (f x) (g x)).
   induction a; simpl in f, g.
     exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
     destruct x.
        exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
        exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
+    exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
+    destruct x.
+       exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
+       exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
     exact (forall x, IHIn (f x) (g x)).
 Defined. 
 
@@ -162,6 +178,8 @@ Definition variance_of_argument_class : Argument_Class -> option variance.
  exact None.
  exact (Some v).
  exact None.
+ exact (Some v).
+ exact None.
 Defined.
 
 Definition opposite_direction :=
@@ -185,15 +203,55 @@ Inductive check_if_variance_is_respected :
      forall dir,
       check_if_variance_is_respected (Some Contravariant) dir (opposite_direction dir).
 
+Inductive Reflexive_Relation_Class : Type :=
+   RSymmetricReflexive :
+     forall A Aeq, @is_symmetric A Aeq -> is_reflexive Aeq -> Reflexive_Relation_Class
+ | RAsymmetricReflexive :
+     forall A Aeq, @is_reflexive A Aeq -> Reflexive_Relation_Class
+ | RLeibniz : Type -> Reflexive_Relation_Class.
+
+Inductive Areflexive_Relation_Class  : Type :=
+ | ASymmetric : forall A Aeq, @is_symmetric A Aeq -> Areflexive_Relation_Class
+ | AAsymmetric : forall A (Aeq : A -> A -> Prop), Areflexive_Relation_Class.
+
+Definition relation_class_of_reflexive_relation_class:
+ Reflexive_Relation_Class -> Relation_Class.
+ induction 1.
+   exact (SymmetricReflexive _ i i0).
+   exact (AsymmetricReflexive tt i).
+   exact (Leibniz _ T).
+Defined.
+
+Definition relation_class_of_areflexive_relation_class:
+ Areflexive_Relation_Class -> Relation_Class.
+ induction 1.
+   exact (Symmetric _ i).
+   exact (Asymmetric tt Aeq).
+Defined.
+
+Definition carrier_of_reflexive_relation_class :=
+ fun R => carrier_of_relation_class (relation_class_of_reflexive_relation_class R).
+
+Definition carrier_of_areflexive_relation_class :=
+ fun R => carrier_of_relation_class (relation_class_of_areflexive_relation_class R).
+
+Definition relation_of_areflexive_relation_class :=
+ fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R).
+
 Inductive Morphism_Context Hole dir : Relation_Class -> rewrite_direction ->  Type :=
     App :
       forall In Out dir',
         Morphism_Theory In Out -> Morphism_Context_List Hole dir dir' In ->
            Morphism_Context Hole dir Out dir'
-  | Toreplace : Morphism_Context Hole dir Hole dir
-  | Tokeep :
+  | ToReplace : Morphism_Context Hole dir Hole dir
+  | ToKeep :
      forall S dir',
-      carrier_of_relation_class S -> Morphism_Context Hole dir S dir'
+      carrier_of_reflexive_relation_class S ->
+        Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
+ | ProperElementToKeep :
+     forall S dir' (x: carrier_of_areflexive_relation_class S),
+      relation_of_areflexive_relation_class S x x ->
+        Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
 with Morphism_Context_List Hole dir :
    rewrite_direction -> Arguments -> Type
 :=
@@ -287,9 +345,11 @@ Theorem apply_morphism_compatibility_Right2Left:
     destruct a; simpl in H; hnf in H0.
           apply H; exact H0.
           destruct v; simpl in H0; apply H; exact H0.
+          apply H; exact H0.
+          destruct v; simpl in H0; apply H; exact H0.
           rewrite H0; apply H; exact H0.
 
-    simpl in m1, m2, args1, args2, H0 |- *.
+   simpl in m1, m2, args1, args2, H0 |- *.
    destruct args1; destruct args2; simpl.
    destruct H0.
    simpl in H.
@@ -304,6 +364,16 @@ Theorem apply_morphism_compatibility_Right2Left:
        apply IHIn.
          apply H; exact H0.       
           exact H1.
+     apply IHIn.
+       apply H; exact H0.
+       exact H1.
+     destruct v.
+       apply IHIn.
+         apply H; exact H0.
+         exact H1.
+       apply IHIn.
+         apply H; exact H0.       
+          exact H1.
     rewrite H0; apply IHIn.
       apply H.
       exact H1.
@@ -322,6 +392,8 @@ Theorem apply_morphism_compatibility_Left2Right:
     destruct a; simpl in H; hnf in H0.
           apply H; exact H0.
           destruct v; simpl in H0; apply H; exact H0.
+          apply H; exact H0.
+          destruct v; simpl in H0; apply H; exact H0.
           rewrite H0; apply H; exact H0.
 
     simpl in m1, m2, args1, args2, H0 |- *.
@@ -339,6 +411,12 @@ Theorem apply_morphism_compatibility_Left2Right:
        apply IHIn.
          apply H; exact H0.       
           exact H1.
+       apply IHIn.
+         apply H; exact H0.
+         exact H1.
+       apply IHIn.
+         destruct v; simpl in H, H0; apply H; exact H0. 
+          exact H1.
     rewrite H0; apply IHIn.
       apply H.
       exact H1.
@@ -355,6 +433,7 @@ Definition interp :
    exact (apply_morphism _ _ (Function m) X).
    exact H.
    exact c.
+   exact x.
    simpl;
      rewrite <-
        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
@@ -380,6 +459,7 @@ Definition interp_relation_class_list :
    exact (apply_morphism _ _ (Function m) X).
    exact H.
    exact c.
+   exact x.
    simpl;
      rewrite <-
        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
@@ -427,17 +507,27 @@ Theorem setoid_rewrite:
      reflexivity.
      reflexivity.
 
+  destruct dir'0; exact r.
+
   destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
    unfold get_rewrite_direction; simpl.
      destruct dir'0; destruct dir'';
        (exact H0 ||
         unfold directed_relation_of_argument_class; simpl; apply i; exact H0).
-   (* the following mess with generalize/clear/intros is to help Coq resolving *)
-   (* second order unification problems.                                                                *)
-   generalize m c H0; clear H0 m c; inversion c;
-     generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
-       (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
-   destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
+     (* the following mess with generalize/clear/intros is to help Coq resolving *)
+     (* second order unification problems.                                                                *)
+     generalize m c H0; clear H0 m c; inversion c;
+       generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
+         (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
+     destruct dir'0; destruct dir'';
+       (exact H0 ||
+        unfold directed_relation_of_argument_class; simpl; apply i; exact H0).
+(* the following mess with generalize/clear/intros is to help Coq resolving *)
+     (* second order unification problems.                                                                *)
+     generalize m c H0; clear H0 m c; inversion c;
+       generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
+         (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
+     destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
 
   change
     (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
@@ -453,7 +543,11 @@ Theorem setoid_rewrite:
         inversion c.
           rewrite <- H3; exact H0.
           rewrite (opposite_direction_idempotent dir'0); exact H0.
-          destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
+        destruct dir''; destruct dir'0; (exact H0 || hnf; apply i; exact H0).
+        inversion c.
+          rewrite <- H3; exact H0.
+          rewrite (opposite_direction_idempotent dir'0); exact H0.
+        destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
      exact H1.
 Qed.