169 lines
4.4 KiB
Coq
169 lines
4.4 KiB
Coq
(* http://poleiro.info/posts/2019-08-06-contravariance-and-recursion.html *)
|
|
Require Import Lia.
|
|
|
|
Inductive type : Type :=
|
|
| Top: type
|
|
| Int: type
|
|
| Arrow: type -> type -> type.
|
|
|
|
Inductive subtype : type -> type -> Type :=
|
|
| STop: forall t:type, subtype t Top
|
|
| SIdty: forall t:type, subtype t t
|
|
| SArrow: forall s1 t1 s2 t2:type,
|
|
subtype s1 t1 -> subtype s2 t2 ->
|
|
subtype (Arrow s2 t1) (Arrow s1 t2).
|
|
|
|
Fail Fixpoint isSubType (a b:type): bool :=
|
|
match a, b with
|
|
| _, Top => true
|
|
| Top, _ => false
|
|
| Int, Int => true
|
|
| Arrow a1 b1, Arrow a2 b2 =>
|
|
andb (isSubType b1 b2) (isSubType a2 a1)
|
|
| _, _ => false
|
|
end.
|
|
|
|
Fixpoint isSubType (flag:bool) (a b:type): bool :=
|
|
match a, b with
|
|
| _, Top => true
|
|
| Top, _ => false
|
|
| Int, Int => true
|
|
| Arrow a1 b1, Arrow a2 b2 =>
|
|
andb (isSubType flag b1 b2) (isSubType (negb flag) a2 a1)
|
|
| _, _ => false
|
|
end.
|
|
|
|
|
|
Fixpoint psum (t:type) : nat :=
|
|
match t with
|
|
| Arrow s t' => (psum s) + (psum t')
|
|
| _ => 1
|
|
end.
|
|
Definition structFn (s t:type) : nat := (psum s) + (psum t).
|
|
Compute psum (Arrow (Arrow Int Int) (Arrow Int Int)).
|
|
Definition structFn' (st:type*type) : nat :=
|
|
(psum (fst st)) + (psum (snd st)).
|
|
Compute psum (Arrow (Arrow Int Int) (Arrow Int Int)).
|
|
|
|
Require Import FunInd.
|
|
Require Import Arith.
|
|
Require Import Program.Wf.
|
|
(* Error: The reference Arith.Wf_nat.ltof was not found in the current environment. *)
|
|
|
|
Require Import Recdef.
|
|
|
|
Program Fixpoint isSubtype (s t:type)
|
|
{measure( psum (Arrow s t))}: bool :=
|
|
match s, t with
|
|
| _, Top => true
|
|
| Int, Int => true
|
|
| Arrow s1 t1, Arrow s2 t2 =>
|
|
andb (isSubtype s2 s1) (isSubtype t1 t2)
|
|
| _, _ => false
|
|
end.
|
|
Next Obligation.
|
|
simpl.
|
|
lia.
|
|
(* rewrite (Nat.add_comm (psum s2) (psum t2)). *)
|
|
(* Check Nat.add_assoc. *)
|
|
(* rewrite (Nat.add_assoc (psum s2) (psum t2)). *)
|
|
|
|
Function isSubtype (s t:type) {measure psum (Arrow s t)}: bool :=
|
|
match s, t with
|
|
| _, Top => true
|
|
| Int, Int => true
|
|
| Arrow s1 t1, Arrow s2 t2 =>
|
|
andb (isSubtype s2 s1) (isSubtype t1 t2)
|
|
| _, _ => false
|
|
end.
|
|
|
|
Function isSubtype (s t:type) {measure structFn' (s,t)}: bool :=
|
|
match s, t with
|
|
| _, Top => true
|
|
| Int, Int => true
|
|
| Arrow s1 t1, Arrow s2 t2 =>
|
|
andb (isSubtype s2 s1) (isSubtype t1 t2)
|
|
| _, _ => false
|
|
end.
|
|
Program Fixpoint isSubtype (s t:type) {measure psum}: bool :=
|
|
match s, t with
|
|
| _, Top => true
|
|
| Int, Int => true
|
|
| Arrow s1 t1, Arrow s2 t2 =>
|
|
andb (isSubtype s2 s1) (isSubtype t1 t2)
|
|
| _, _ => false
|
|
end.
|
|
|
|
Function isSubtype (s t:type) {measure structFn' (s,t)} : bool :=
|
|
match s, t with
|
|
| _, Top => true
|
|
| Int, Int => true
|
|
| Arrow s1 t1, Arrow s2 t2 =>
|
|
andb (isSubtype s2 s1) (isSubtype t1 t2)
|
|
| _, _ => false
|
|
end.
|
|
|
|
Fixpoint isSubtype (s t:type) (flag:bool) {struct flag} : bool :=
|
|
match s, t with
|
|
| Top, Top => true
|
|
| Top, _ => negb (negb flag)
|
|
| _, Top => flag
|
|
| Int, Int => true
|
|
| Arrow s1 t1, Arrow s2 t2 =>
|
|
andb (isSubtype s2 s1 flag) (isSubtype t1 t2 (negb flag))
|
|
| _, _ => false
|
|
end.
|
|
|
|
|
|
Fail Fixpoint isSubtype (s t:type) {struct s} : bool :=
|
|
match s, t with
|
|
| _, Top => true
|
|
| Int, Int => true
|
|
| Arrow s1 t1, Arrow s2 t2 =>
|
|
andb (isSubtype s2 s1) (isSubtype t1 t2)
|
|
| _, _ => false
|
|
end.
|
|
(* The command has indeed failed with message: *)
|
|
(* Recursive definition of isSubtype is ill-formed. *)
|
|
(* In environment *)
|
|
(* isSubtype : type -> type -> bool *)
|
|
(* s : type *)
|
|
(* t : type *)
|
|
(* s1 : type *)
|
|
(* t1 : type *)
|
|
(* s2 : type *)
|
|
(* t2 : type *)
|
|
(* Recursive call to isSubtype has principal argument equal to *)
|
|
(* "s2" instead of one of the following variables: *)
|
|
(* "s1" "t1". *)
|
|
(* Recursive definition is: *)
|
|
(* "fun s t : type => *)
|
|
(* match s with *)
|
|
(* | Top => match t with *)
|
|
(* | Top => true *)
|
|
(* | _ => false *)
|
|
(* end *)
|
|
(* | Int => match t with *)
|
|
(* | Arrow _ _ => false *)
|
|
(* | _ => true *)
|
|
(* end *)
|
|
(* | Arrow s1 t1 => *)
|
|
(* match t with *)
|
|
(* | Top => true *)
|
|
(* | Int => false *)
|
|
(* | Arrow s2 t2 => *)
|
|
(* (isSubtype s2 s1 && isSubtype t1 t2)%bool *)
|
|
(* end *)
|
|
(* end". *)
|
|
|
|
|
|
Fail Fixpoint isSubtype (s t:type): bool :=
|
|
match s, t with
|
|
| _, Top => true
|
|
| Int, Int => true
|
|
| Arrow s1 t1, Arrow s2 t2 =>
|
|
andb (isSubtype s2 s1) (isSubtype t1 t2)
|
|
| _, _ => false
|
|
end.
|
|
(* Error: Cannot guess decreasing argument of fix. *)
|