From d16ab1aaa77ed3a9b052d12496d92c102288b704 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 29 Jan 2021 19:37:53 +0100 Subject: [PATCH] Add some tests. --- tests/solve_proper.v | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/tests/solve_proper.v b/tests/solve_proper.v index d4e4d665..abd7911c 100644 --- a/tests/solve_proper.v +++ b/tests/solve_proper.v @@ -22,3 +22,38 @@ Section tests. Goal Proper (pointwise_relation nat (≡) ==> (≡)) test3. Proof. solve_proper. Qed. End tests. + +(** The following tests are inspired by Iris's [ofe] structure (here, simplified +to just a type an arbitrary relation), and the discrete function space [A -d> B] +on a Type [A] and OFE [B]. The tests occur when proving [Proper]s for +higher-order functions, which typically occurs while defining functions using +Iris's [fixpoint] operator. *) +Record setoid := + Setoid { setoid_car :> Type; setoid_equiv : relation setoid_car }. +Arguments setoid_equiv {_} _ _. + +Definition myfun (A : Type) (B : setoid) := A → B. +Definition myfun_equiv {A B} : relation (myfun A B) := + pointwise_relation _ setoid_equiv. +Definition myfunS (A : Type) (B : setoid) := Setoid (myfun A B) myfun_equiv. + +Section setoid_tests. + Context {A : setoid} (f : A → A) (h : A → A → A). + Context `{!Proper (setoid_equiv ==> setoid_equiv) f, + !Proper (setoid_equiv ==> setoid_equiv ==> setoid_equiv) h}. + + Definition setoid_test1 (rec : myfunS nat A) : myfunS nat A := + λ n, h (f (rec n)) (rec n). + Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test1. + Proof. solve_proper. Qed. + + Definition setoid_test2 (rec : myfunS nat (myfunS nat A)) : myfunS nat A := + λ n, h (f (rec n n)) (rec n n). + Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test2. + Proof. solve_proper. Qed. + + Definition setoid_test3 (rec : myfunS nat A) : myfunS nat (myfunS nat A) := + λ n m, h (f (rec n)) (rec m). + Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test3. + Proof. solve_proper. Qed. +End setoid_tests. -- GitLab