Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
eb7bb11c
Commit
eb7bb11c
authored
Sep 17, 2014
by
JeanChristophe Filliâtre
Browse files
doc: transformation induction_ty_lex
parent
6d7a446e
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
32 additions
and
9 deletions
+32
9
doc/technical.tex
doc/technical.tex
+32
9
No files found.
doc/technical.tex
View file @
eb7bb11c
...
...
@@ 184,22 +184,45 @@ each $x_1 \dots x_n$ occurs at most once in all the $e_i$.
\subsection
{
Induction Transformations
}
\begin{itemize}
\item
Induction on an algebraic data type:
\verb

induction_ty_lex

\index
{
inductiontylex@
\verb
+
induction_ty_lex
+
}
[TO BE COMPLETED]
\begin{description}
\item
[induction\_ty\_lex]
:
\index
{
inductiontylex@
\verb
+
induction_ty_lex
+
}
This transformation performs structural, lexicographic induction on
goals involving universally quantified variables of algebraic data
types, such as lists, trees, etc. For instance, it transforms the
following goal
\begin{whycode}
goal G: forall l: list 'a. length l >= 0
\end{whycode}
into this one:
\begin{whycode}
goal G :
forall l:list 'a.
match l with
 Nil > length l >= 0
 Cons a l1 > length l1 >= 0 > length l >= 0
end
\end{whycode}
When induction can be applied to several variables, the transformation
picks one heuristically. A label
\verb

induction

can be used to
force induction over one particular variable,
\emph
{
e.g.
}
,
\begin{whycode}
goal G: forall l1 "induction" l2 l3: list 'a.
l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
\end{whycode}
If such a label is used on several variables, a lexicographic
induction is performed on these variables, from left to right.
\item
Induction on
a
inductive predicate
:
\item
[]
Induction on inductive predicate
s.
[TO BE COMPLETED]
\end{
itemize
}
\end{
description
}
\subsection
{
Simplification by Computation
}
Th
o
se transformations simplif
ies
the goal by applying several kind of
simplification
s
. The transformations differ only by the kind of rules they
Th
e
se transformations simplif
y
the goal by applying several kind
s
of
simplification. The transformations differ only by the kind of rules they
apply:
\verb

compute_in_goal

aggressively apply all known
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment