The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hi Matthieu,

Thanks, for the pointers. That did get me started, but not quite off the
ground yet. I now have examples of (simple) rewrites that succeed in the
Prop and in the Type formulations. But the first thing involving
contravariance fails in the Type formulation. (I need preorders and
contravariant morphisms)

I get failures involving do_subrelation such as the one below. I
attached two files, the formulation in Prop where the rewrite works and
the one in Type where it fails.

Tactic failure: setoid rewrite failed: Unable to satisfy the following
constraints:
UNDEFINED EVARS:
 ?X57==[s |- crelation form] (internal placeholder) {?c}
 ?X58==[s |- crelation form] (internal placeholder) {?c0}
 ?X59==[s (do_subrelation:=do_subrelation)
         |- Proper
              ((fun x y : form => prv (x ---> y)) ==>
               ?X58@{__:=s} ==> ?X57@{__:=s}) Imp] (internal
placeholder) {?p}
 ?X60==[s |- ProperProxy ?X58@{__:=s} s] (internal placeholder) {?p0}
 ?X61==[s (do_subrelation:=do_subrelation)
         |- Proper (?X57@{__:=s} ==> flip arrow) prv] (internal
placeholder) {?p1}
.

I don't know enough about the internals of type class resolution to make
sense of this. Maybe you know what is going wrong here.

Best,
Christian

On 09/10/17 10:16, Matthieu Sozeau wrote:
> Hi Christian,
> 
>   indeed there is a variant of setoid_rewrite for computational relations,
> which requires you to use the CMorphisms and CRelationClasses (C for
> computational) 
> libraries instead of the usual Morphisms and RelationClasses libraries. 
> Using the definitions in there you can define Proper instances for your
> constants where the relation is computational (typically using iffT
> instead of iff, arrow instead
> of logical implication), to be used by setoid_rewrite.
> 
> Hope this helps,
> -- Matthieu
> 
> On Sun, Oct 8, 2017 at 11:40 PM Christian Doczkal
> <christian.doczkal AT ens-lyon.fr
>  
> <mailto:christian.doczkal AT ens-lyon.fr>>
> wrote:
> 
>     Hello everyone,
> 
>     Is it possible to use setoid rewriting when constructing inhabitants of
>     type families (X -> Type).
> 
>     I have some developments proving meta-theoretic properties of proof
>     systems (e.g., Hilbert style systems or sequent systems). So far I've
>     been formalizing proof systems as inductive predicates of type:
> 
>             formula (or sequent) -> Prop
> 
>     The main reason for this is that I make extensive use of setoid
>     rewriting to replace formulas by provably equivalent ones.
> 
>     However, treating proofs of deeply embedded calculi as computational
>     objects seems more natural to me. Moreover, this allow defining
>     functions from proofs to nat (e.g, for the size of a proof). However, I
>     would still want to use setoid rewriting where the shape of the proof is
>     irrelevant.
> 
>     I recall being told that prior to the introduction of universe
>     polymorphism, setoid could not be used for type families. So now that we
>     have universe polymorphism, is this reasonable now? If so, what would I
>     need to do to set this up?
> 
>     Thanks in advance,
>     Christian
> 
Require Import Setoid Morphisms RelationClasses Basics.

Inductive form := 
| Var : nat -> form
| Imp : form -> form -> form
| FF : form.

Notation "s ---> t" := (Imp s t) (at level 35, right associativity).
Definition Neg s := Imp s FF.

Parameter prv : form -> Prop.

Axiom axS : forall s t u, prv ((u ---> s ---> t) ---> (u ---> s) ---> u ---> t).
Axiom axK : forall s t, prv (s ---> t ---> s).
Axiom MP : forall s t, prv (s ---> t) -> prv s -> prv t.
Axiom axDN : forall s, prv (Neg (Neg s) ---> s).

Lemma axI s : prv (s ---> s).
Admitted.

Definition prv_imp s t := prv (Imp s t).

Instance prv_order : PreOrder prv_imp.
Proof. split. Admitted.

Instance prv_mor : Proper (prv_imp ++> impl) prv.
Proof. intros s t. unfold impl, prv_imp. now apply MP. Qed.

Instance Imp_mor : Proper (prv_imp --> prv_imp ++> prv_imp) Imp.
Proof. 
  intros s t Hst u v Huv. unfold flip, prv_imp in *. 
Admitted.

Lemma axFE s : prv (Imp FF s).
Proof. rewrite <- (axDN s). now apply axK. Qed.

Lemma axFE' s : prv (Imp FF s).
Proof. rewrite -> axFE. apply axI. Qed.

Require Import Setoid CMorphisms CRelationClasses.

Inductive form := 
| Var : nat -> form
| Imp : form -> form -> form
| FF : form.

Notation "s ---> t" := (Imp s t) (at level 35, right associativity).
Definition Neg s := Imp s FF.

Parameter prv : form -> Type.

Axiom axS : forall s t u, prv ((u ---> s ---> t) ---> (u ---> s) ---> u ---> t).
Axiom axK : forall s t, prv (s ---> t ---> s).
Axiom MP : forall s t, prv (s ---> t) -> prv s -> prv t.
Axiom axDN : forall s, prv (Neg (Neg s) ---> s).

Lemma axI s : prv (s ---> s).
Admitted.

Definition prv_imp s t := prv (Imp s t).

Instance prv_order : PreOrder prv_imp.
Proof. split. Admitted.

Instance prv_mor : Proper (prv_imp ++> arrow) prv.
Proof. intros s t. unfold arrow, prv_imp. now apply MP. Qed.

Instance Imp_mor : Proper (prv_imp --> prv_imp ++> prv_imp) Imp.
Proof. 
  intros s t Hst u v Huv. unfold flip, prv_imp in *. 
Admitted.

Lemma axFE s : prv (Imp FF s).
Proof. rewrite <- (axDN s). now apply axK. Qed.

Lemma axFE' s : prv (Imp FF s).
Proof. Fail rewrite -> axFE.