Reasoning

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% This example demonstrates how to use schematic polymorphism to
%% prove properties about inductively defined polymorphic definitions
%% at the reasoning level
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% A schematic definition for append
Define app : list A -> list A -> list A -> prop by
  app nil L L;
  app (X :: L1) L2 (X :: L3) := app L1 L2 L3.

% Append is deterministic in its third argument
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.
  % Case: L1 = nil, L2 = L3
  case H2. search.
  % Inductive case
  case H2. apply IH to H3 H4. search.
% The determinacy property at some particular type instances
Kind nat type.

% Apply app_det to list of natural numbers
Theorem app_det_nat : forall (L1: list nat) L2 L3 L3',
  app L1 L2 L3 -> app L1 L2 L3' -> L3 = L3'.
  intros. apply app_det to H1 H2. search.
% Apply app_det to polymorphic lists of lists
Theorem app_det_list[B] : forall (L1 : list (list B)) L2 L3 L3',
  app L1 L2 L3 -> app L1 L2 L3' -> L3 = L3'.
  intros. apply app_det to H1 H2. search.