sig schm_poly_tst. type app list A -> list A -> list A -> o. kind i type. type cst A -> i. type pred i -> o.

module schm_poly_tst. app nil L L. app (X :: L1) L2 (X :: L3) :- app L1 L2 L3. pred (cst X).

Click on a command or tactic to see a detailed view of its use.

Specification "schm_poly_tst". % Set types on. % Set instantiations on. Define append : list A -> list A -> list A -> prop by append nil L L; append (X :: L1) L2 (X :: L3) := append L1 L2 L3. Theorem append_det[A] : forall (L1: list A) L2 L3 L3', append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'. Theorem oappend_det : forall (L1: list o) L2 L3 L3', append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'. Theorem append_det1[A] : forall (L1: list A) L2 L3 L3', append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'. Theorem append_det2[A] : forall (L1: list A) L2 L3 L3', append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'. Theorem append_det3[A] : forall (L1: list A) L2 L3 L3', append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'. %% Do not support types with a variable as its target % Type fst,snd list A -> A. Type p A -> o. Define eq : A -> A -> prop by eq M M. Theorem tst [A,B] : forall (X:A) (Y:B), eq (p X) (p Y) -> false.intros. %% The following case analysis should report an error that %% generic type variables cannot be instantiated % case H1. skip.Theorem inst_gen_var1[A,B] : forall (X:A) (Y:B), p X = p Y -> false.intros. %% The following case analysis should report an error that %% generic type variables cannot be instantiated % case H1. skip.Theorem inst_gen_var2[A] : forall (X:A) (Y:o), p X = p Y -> false. Theorem inst_gen_var3[A] : forall (X:i) (Y:o), p X = p Y -> false. Theorem member_prune[A,B] : forall M (L:list A), nabla (x:B), member (M x) L -> exists M', M = y\M'. Theorem olist_mem_prune : forall M (L:list o), nabla (x:o), member (M x) L -> exists M', M = y\M'. Theorem member_prune1[A,B] : forall M (L:list A), nabla (x:B), member (M x) L -> exists M', M = y\M'. Theorem member_prune2[A,B] : forall M (L:list A), nabla (x:B), member (M x) L -> exists M', M = y\M'. Theorem member_prune3[A,B] : forall M (L:list A), nabla (x:i), member (M x) L -> exists M', M = y\M'. Theorem member_prune4[A,B] : forall M (L:list A), nabla (x:i), member (M x) L -> exists M', M = y\M'. Theorem olist_mem_prune_bc : forall M (L:list o), nabla (x:o), member (M x) L -> exists M', M = y\M'. Theorem member_prune1_bc[A,B] : forall M (L:list A), nabla (x:B), member (M x) L -> exists M', M = y\M'. Theorem app_det[A] : forall (L1: list A) L2 L3 L3', {app L1 L2 L3} -> {app L1 L2 L3'} -> L3 = L3'. Theorem app_search[A] : forall (X:A) L, {app (X :: nil) L (X :: L)}. Theorem ty_fdet_left[A] : forall (X:A), {pred (cst X)} -> true. Theorem ty_fdet_right[A] : forall (X:A), {pred (cst X)}. Theorem ty_not_fdet_left : forall M, {pred M} -> false.intros. %% The following case analysis should report an error because the %% type variable in the clause cannot be fully instantiated by unification % case H1. skip.Theorem ty_not_fdet_right : forall M, {pred M}.%% The following search should fail because the type variable in the %% clause cannot be fully instantiated by unification %search. skip.