Commit 4e212696 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'issue_311' into 'master'

Issue 311

Closes #311

See merge request !130
parents 6d112dd4 0a4ec4c2
......@@ -32,6 +32,9 @@ Transformations
* `induction_arg_ty_lex` is now equivalent to `induction_ty_lex`
* `induction_arg_pr` now takes an optional argument that indicates what to
generalize in the induction
* `destruct` now destruct `not p` into `p -> false`. `destruct_rec` is
allowed to further destruct afterwards.
`destruct` can also destruct `true` and `false`.
* display of counterexamples in the Task view has been improved
use list.List
use list.Length
use int.Int
constant x: int
predicate p int
axiom H: not (p 0)
axiom H1: p 0
goal g: false
axiom H2: false
goal g5: p 5
axiom H3: true
goal g6: p 5
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
<why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="20" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/>
<path name="311_destruct.mlw"/>
<theory name="Top" proved="true">
<goal name="g" proved="true">
<transf name="destruct" proved="true" arg1="H">
<goal name="g.0" proved="true">
<transf name="destruct" proved="true" arg1="H">
<goal name="g.0.0" expl="destruct premise" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<goal name="g.0.1" proved="true">
<transf name="destruct" proved="true" arg1="H">
<transf name="destruct_rec" proved="true" arg1="H">
<goal name="g.0" expl="destruct premise" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<goal name="g5" proved="true">
<transf name="destruct" proved="true" arg1="H2">
<goal name="g6" proved="true">
<transf name="destruct" proved="true" arg1="H3">
<goal name="g6.0" proved="true">
<transf name="destruct" proved="true" arg1="H2">
......@@ -248,6 +248,10 @@ let destruct_fmla ~recursive (t: term) =
match t.t_node with
| Tfalse ->
| Ttrue ->
| Tbinop (Tand, t1, t2) ->
let l1 = destruct_fmla_exception ~toplevel:false t1 in
let l2 = destruct_fmla_exception ~toplevel:false t2 in
......@@ -321,6 +325,9 @@ let destruct_fmla ~recursive (t: term) =
(* The hypothesis is trivial because Cs1 <> Cs2 thus useless *)
| Tnot t1 ->
(* Keep toplevel: this is considered an implication *)
destruct_fmla_exception ~toplevel (t_implies t1 t_false)
| Tif (t1, t2, t3) ->
let ts2 =
destruct_fmla_exception ~toplevel:false t2 |>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment