# Reasoning

[View schm_fail]

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

```%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% This example demonstrates when schematic polymorphism fails to prove
%% properties about polymorphic specifications
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Define eq : A -> A -> prop by
eq X X.

Type p   A -> o.

Theorem eq_non_schm[A,B] : forall (X:A) (Y:B),
eq (p X) (p Y) -> false.
intros.
%% The following case analysis fails for the following reason.
%% Whether (p X) is equal to (p Y) depends on whether X and Y has
%% identical types, i.e., whether A and B can be made equal. Since A
%% and B are treated as "black boxes", examination of their identity
%% is not allowed.

% case H1.
skip.
%% The following is a theorem that does not have
%% a schematic proof.
Theorem true_thm_with_no_schematic_proof [A,B]:
forall (X:A) (F:A -> B), exists (Y:B),
(eq (p X) (p Y)) \/ (eq (p X) (p Y) -> false).
%% This theorem has a proof as follows:
%% Case 1: A = B.
%%   We choose Y to be X and show the right branch holds.
%% Case 2: A =/= B.
%%   We choose Y to be (F X) and then try to prove the right branch.
%%   Since (p X) and (p Y) has different predicate heads,
%%   the right branch is trivially true.
%%
%% However, since the above proof inspects the types for A and B,
%% it is not a schematic proof. In fact, the above theorem, also provable,
%% does not have a schematic proof.
skip.
```