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'.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H4. search.
Theorem oappend_det : forall (L1: list o) L2 L3 L3',
append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.
intros. apply append_det[o] to H1 H2. search.
Theorem append_det1[A] : forall (L1: list A) L2 L3 L3',
append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.
intros. apply append_det[A] to H1 H2. search.
Theorem append_det2[A] : forall (L1: list A) L2 L3 L3',
append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.
intros. apply append_det[_] to H1 H2. search.
Theorem append_det3[A] : forall (L1: list A) L2 L3 L3',
append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.
intros. apply append_det to H1 H2. search.
%% 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.
intros.
% case H1.
skip.
Theorem inst_gen_var3[A] : forall (X:i) (Y:o),
p X = p Y -> false.
intros. case H1.
Theorem member_prune[A,B] : forall M (L:list A), nabla (x:B),
member (M x) L -> exists M', M = y\M'.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Theorem olist_mem_prune : forall M (L:list o), nabla (x:o),
member (M x) L -> exists M', M = y\M'.
intros. apply member_prune[o,o] to H1. search.
Theorem member_prune1[A,B] : forall M (L:list A), nabla (x:B),
member (M x) L -> exists M', M = y\M'.
intros. apply member_prune[A,B] to H1. search.
Theorem member_prune2[A,B] : forall M (L:list A), nabla (x:B),
member (M x) L -> exists M', M = y\M'.
intros. apply member_prune[_,B] to H1. search.
Theorem member_prune3[A,B] : forall M (L:list A), nabla (x:i),
member (M x) L -> exists M', M = y\M'.
intros. apply member_prune[_,i] to H1. search.
Theorem member_prune4[A,B] : forall M (L:list A), nabla (x:i),
member (M x) L -> exists M', M = y\M'.
intros. apply member_prune to H1. search.
Theorem olist_mem_prune_bc : forall M (L:list o), nabla (x:o),
member (M x) L -> exists M', M = y\M'.
intros. backchain member_prune[o,o].
Theorem member_prune1_bc[A,B] : forall M (L:list A), nabla (x:B),
member (M x) L -> exists M', M = y\M'.
intros. backchain member_prune[A,B].
Theorem app_det[A] : forall (L1: list A) L2 L3 L3',
{app L1 L2 L3} -> {app L1 L2 L3'} -> L3 = L3'.
induction on 1. intros. case H1 (keep).
case H2. search.
case H2. apply IH to H3 H4. search.
Theorem app_search[A] : forall (X:A) L,
{app (X :: nil) L (X :: L)}.
search.
Theorem ty_fdet_left[A] : forall (X:A),
{pred (cst X)} -> true.
intros. case H1. search.
Theorem ty_fdet_right[A] : forall (X:A),
{pred (cst X)}.
search.
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.
