Skip to content

use Program less in stdlib #19797

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
andres-erbsen wants to merge 1 commit into from
Closed

use Program less in stdlib #19797

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 10 additions & 11 deletions theories/Arith/PeanoNat.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,17 +31,16 @@ Set Inline Level 50.
(** All operations are well-defined (trivial here since eq is Leibniz) *)

Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence.
Local Obligation Tactic := simpl_relation.
#[global] Program Instance succ_wd : Proper (eq==>eq) S.
#[global] Program Instance pred_wd : Proper (eq==>eq) pred.
#[global] Program Instance add_wd : Proper (eq==>eq==>eq) plus.
#[global] Program Instance sub_wd : Proper (eq==>eq==>eq) minus.
#[global] Program Instance mul_wd : Proper (eq==>eq==>eq) mult.
#[global] Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
#[global] Program Instance div_wd : Proper (eq==>eq==>eq) div.
#[global] Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
#[global] Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
#[global] Program Instance testbit_wd : Proper (eq==>eq==>eq) testbit.
#[global] Instance succ_wd : Proper (eq==>eq) S := _.
#[global] Instance pred_wd : Proper (eq==>eq) pred := _.
#[global] Instance add_wd : Proper (eq==>eq==>eq) plus := _.
#[global] Instance sub_wd : Proper (eq==>eq==>eq) minus := _.
#[global] Instance mul_wd : Proper (eq==>eq==>eq) mult := _.
#[global] Instance pow_wd : Proper (eq==>eq==>eq) pow := _.
#[global] Instance div_wd : Proper (eq==>eq==>eq) div := _.
#[global] Instance mod_wd : Proper (eq==>eq==>eq) modulo := _.
#[global] Instance lt_wd : Proper (eq==>eq==>iff) lt := _.
#[global] Instance testbit_wd : Proper (eq==>eq==>eq) testbit := _.

(** Bi-directional induction. *)

Expand Down
21 changes: 7 additions & 14 deletions theories/Classes/CEquivalence.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ Set Implicit Arguments.
Unset Strict Implicit.

Generalizable Variables A R eqA B S eqB.
Local Obligation Tactic := try solve [simpl_crelation].

Local Open Scope signatureT_scope.

Expand Down Expand Up @@ -54,18 +53,13 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
(** Shortcuts to make proof search easier. *)

#[global]
Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.
Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv := _.

#[global]
Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv := _.

#[global]
Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.

Next Obligation.
Proof. intros A R sa x y z Hxy Hyz.
now transitivity y.
Qed.
Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv := _.

Arguments equiv_symmetric {A R} sa x y : rename.
Arguments equiv_transitive {A R} sa x y z : rename.
Expand Down Expand Up @@ -119,14 +113,13 @@ Section Respecting.
eqb : Equivalence B (R' : crelation B)) : Type :=
{ morph : A -> B & respectful R R' morph morph }.

Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
Equivalence (fun (f g : respecting eqa eqb) =>
forall (x y : A), R x y -> R' (projT1 f x) (projT1 g y)).

Solve Obligations with unfold respecting in * ; simpl_crelation ; program_simpl.

Next Obligation.
Proof.
split.
{ unfold respecting in * ; simpl_crelation ; program_simpl. }
{ unfold respecting in * ; simpl_crelation ; program_simpl. }
intros. intros f g h H H' x y Rxy.
unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder.
Qed.
Expand Down
68 changes: 23 additions & 45 deletions theories/Classes/CMorphisms.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@ Require Import Stdlib.Program.Tactics.
Require Export Stdlib.Classes.CRelationClasses.

Generalizable Variables A eqA B C D R RA RB RC m f x y.
Local Obligation Tactic := try solve [ simpl_crelation ].

Local Arguments transitivity {A R Transitive x} y {z}.

Expand Down Expand Up @@ -277,11 +276,10 @@ Section GenericInstances.
(** We can build a PER on the Coq function space if we have PERs on the domain and
codomain. *)

Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').

Next Obligation.
Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
Proof with auto.
intros A R H B R' H0 x y z X X0 x0 y0 X1.
split. { simpl_crelation. }
intros x y z X X0 x0 y0 X1.
assert(R x0 x0).
- eapply transitivity with y0... now apply symmetry.
- eapply transitivity with (y x0)...
Expand All @@ -292,78 +290,64 @@ Section GenericInstances.
(** The complement of a crelation conserves its proper elements. *)

(** The [flip] too, actually the [flip] instance is a bit more general. *)
Program Definition flip_proper
Definition flip_proper
`(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
Proper (RB ==> RA ==> RC) (flip f) := _.

Next Obligation.
Proper (RB ==> RA ==> RC) (flip f).
Proof.
intros A B C RA RB RC f mor x y X x0 y0 X0.
intros x y X x0 y0 X0.
apply mor ; auto.
Qed.


(** Every Transitive crelation gives rise to a binary morphism on [impl],
contravariant in the first argument, covariant in the second. *)

Global Program
Global
Instance trans_contra_co_type_morphism
`(Transitive A R) : Proper (R --> R ++> arrow) R.

Next Obligation.
Proof with auto.
intros A R H x y X x0 y0 X0 X1.
intros x y X x0 y0 X0 X1.
apply transitivity with x...
apply transitivity with x0...
Qed.

(** Proper declarations for partial applications. *)

Global Program
Global
Instance trans_contra_inv_impl_type_morphism
`(Transitive A R) {x} : Proper (R --> flip arrow) (R x) | 3.

Next Obligation.
Proof with auto.
intros A R H x x0 y X X0.
intros x0 y X X0.
apply transitivity with y...
Qed.

Global Program
Global
Instance trans_co_impl_type_morphism
`(Transitive A R) {x} : Proper (R ++> arrow) (R x) | 3.

Next Obligation.
Proof with auto.
intros A R H x x0 y X X0.
intros x0 y X X0.
apply transitivity with x0...
Qed.

Global Program
Global
Instance trans_sym_co_inv_impl_type_morphism
`(PER A R) {x} : Proper (R ++> flip arrow) (R x) | 3.

Next Obligation.
Proof with auto.
intros A R H x x0 y X X0.
intros x0 y X X0.
apply transitivity with y... apply symmetry...
Qed.

Global Program Instance trans_sym_contra_arrow_morphism
Global Instance trans_sym_contra_arrow_morphism
`(PER A R) {x} : Proper (R --> arrow) (R x) | 3.

Next Obligation.
Proof with auto.
intros A R H x x0 y X X0.
intros x0 y X X0.
apply transitivity with x0... apply symmetry...
Qed.

Global Program Instance per_partial_app_type_morphism
Global Instance per_partial_app_type_morphism
`(PER A R) {x} : Proper (R ==> iffT) (R x) | 2.

Next Obligation.
Proof with auto.
intros A R H x x0 y X.
intros x0 y X.
split.
- intros ; apply transitivity with x0...
- intros.
Expand All @@ -373,24 +357,20 @@ Section GenericInstances.

(** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)

Global Program
Global
Instance trans_co_eq_inv_arrow_morphism
`(Transitive A R) : Proper (R ==> (@eq A) ==> flip arrow) R | 2.

Next Obligation.
Proof with auto.
intros A R H x y X y0 y1 e X0; destruct e.
intros x y X y0 y1 e X0; destruct e.
apply transitivity with y...
Qed.

(** Every Symmetric and Transitive crelation gives rise to an equivariant morphism. *)

Global Program
Global
Instance PER_type_morphism `(PER A R) : Proper (R ==> R ==> iffT) R | 1.

Next Obligation.
Proof with auto.
intros A R H x y X x0 y0 X0.
intros x y X x0 y0 X0.
split ; intros.
- apply transitivity with x0...
apply transitivity with x... apply symmetry...
Expand All @@ -402,10 +382,8 @@ Section GenericInstances.
Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
Proof. firstorder. Qed.

Global Program Instance compose_proper A B C RA RB RC :
Global Instance compose_proper A B C RA RB RC :
Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C).

Next Obligation.
Proof.
simpl_crelation.
unfold compose. firstorder.
Expand Down
28 changes: 14 additions & 14 deletions theories/Classes/CRelationClasses.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@

Require Export Stdlib.Classes.Init.
Require Import Stdlib.Program.Basics.
Require Import Stdlib.Program.Tactics.

Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.

Expand Down Expand Up @@ -122,19 +121,19 @@ Section Defs.
Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R).
Proof. tauto. Qed.

Program Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
irreflexivity (R:=R).

Program Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
fun x y H => symmetry (R:=R) H.

Program Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
fun x y H H' => asymmetry (R:=R) H H'.

Program Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
fun x y z H H' => transitivity (R:=R) H' H.

Program Lemma flip_Antisymmetric `(Antisymmetric eqA R) :
Lemma flip_Antisymmetric `(Antisymmetric eqA R) :
Antisymmetric eqA (flip R).
Proof. firstorder. Qed.

Expand Down Expand Up @@ -191,7 +190,8 @@ Section Defs.
The instance has low priority as it is always applicable
if only the type is constrained. *)

Global Program Instance eq_equivalence : Equivalence (@eq A) | 10.
Global Instance eq_equivalence : Equivalence (@eq A) | 10.
Proof. split; exact _. Qed.
End Leibniz.

End Defs.
Expand Down Expand Up @@ -273,18 +273,18 @@ Tactic Notation "apply" "*" constr(t) :=
first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].

Require Import Stdlib.Program.Tactics.

Ltac simpl_crelation :=
unfold flip, impl, arrow ; try reduce ; program_simpl ;
try ( solve [ dintuition auto with crelations ]).

Local Obligation Tactic := simpl_crelation.

(** Logical implication. *)

#[global]
Program Instance impl_Reflexive : Reflexive impl.
Instance impl_Reflexive : Reflexive impl. Proof. simpl_crelation. Qed.
#[global]
Program Instance impl_Transitive : Transitive impl.
Instance impl_Transitive : Transitive impl. Proof. simpl_crelation. Qed.

(** Logical equivalence. *)

Expand All @@ -298,11 +298,11 @@ Instance iff_Transitive : Transitive iff := iff_trans.
(** Logical equivalence [iff] is an equivalence crelation. *)

#[global]
Program Instance iff_equivalence : Equivalence iff.
Instance iff_equivalence : Equivalence iff. Proof. split; simpl_crelation. Qed.
#[global]
Program Instance arrow_Reflexive : Reflexive arrow.
Instance arrow_Reflexive : Reflexive arrow. Proof. simpl_crelation. Qed.
#[global]
Program Instance arrow_Transitive : Transitive arrow.
Instance arrow_Transitive : Transitive arrow. Proof. simpl_crelation. Qed.

#[global]
Instance iffT_Reflexive : Reflexive iffT.
Expand Down
Loading