From 208569fe73fe08be5fd9f59c2861a5d7868815cb Mon Sep 17 00:00:00 2001 From: Benedikt Becker Date: Wed, 6 Feb 2019 11:50:51 +0100 Subject: [PATCH] Update examples for recursive destruct of conditionals and matches --- examples/bts/264_destruct_if.mlw | 74 +++++++++--- examples/bts/264_destruct_if/why3session.xml | 114 ++++++++++++++++--- examples/bts/264_destruct_if/why3shapes.gz | Bin 367 -> 879 bytes 3 files changed, 158 insertions(+), 30 deletions(-) diff --git a/examples/bts/264_destruct_if.mlw b/examples/bts/264_destruct_if.mlw index 8cb1c7d8d..a529490a9 100644 --- a/examples/bts/264_destruct_if.mlw +++ b/examples/bts/264_destruct_if.mlw @@ -1,19 +1,22 @@ +use list.List +use list.Length +use int.Int constant x: int predicate p int +(**********************) +(* Simple destruction *) +(**********************) + axiom H: if x = 42 then p 1 else p 2 -goal g: p 3 - -use list.List -use list.Length -use int.Int +goal g: p 0 constant l: list int -axiom H': match l with +axiom H1: match l with | Nil -> p 4 | Cons x y -> p (x+length y) | Cons _ (Cons y Nil) -> p y @@ -21,19 +24,64 @@ axiom H': match l with | Cons _ (Cons _ (Cons _ _)) -> p 5 end -goal g': p 6 +goal g1: p 1 + +(**********************) +(* As and or patterns *) +(**********************) -axiom H'': match l with +axiom H2: match l with | Nil -> p 1 | Cons x Nil | Cons _ (Cons x Nil) -> p x -| Cons _ (Cons _ _ as l') -> p (length l') +| Cons _ (Cons _ _ as l1) -> p (length l1) end -goal g'': p 7 +goal g2: p 2 -axiom H''': match l with -| Cons _ (Cons _ _ as l') as l'' -> p (length l'+length l'') +axiom H3: match l with +| Cons _ (Cons _ _ as l1) as l2 -> p (length l1+length l2) | _ -> p 0 end -goal g''': p 8 \ No newline at end of file +goal g3: p 3 + +(*************************) +(* Recursive destruction *) +(*************************) + +axiom H4: + if p x then + (if p (x+1) then + p 1 + else + p 2) + else p 3 + +goal g4: p 4 + +axiom H5: match l with +| Cons x (Cons y _) -> + if x = y then + p 1 \/ p 2 + else + p 3 /\ p 4 +| _ -> true +end + +(*********************************************************************************) +(* Interaction between recursive destruction of conditionals and of implications *) +(*********************************************************************************) + +goal g5: p 5 + +axiom H6: p 1 -> if p 2 then p 3 else p 4 + +goal g6: p 6 + +axiom H7: if p 1 then p 2 -> p 3 else p 4 + +goal g7: p 7 + +axiom H8: if p 1 then if p 2 then (p 3 -> p 4) else p 5 else p 6 + +goal g8: p 8 \ No newline at end of file diff --git a/examples/bts/264_destruct_if/why3session.xml b/examples/bts/264_destruct_if/why3session.xml index cf490b6ce..9b9c4ae70 100644 --- a/examples/bts/264_destruct_if/why3session.xml +++ b/examples/bts/264_destruct_if/why3session.xml @@ -14,37 +14,117 @@ - - - + + + - + - + - + - + - - - + + + - + - + - + - - - + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/bts/264_destruct_if/why3shapes.gz b/examples/bts/264_destruct_if/why3shapes.gz index c4843c536d50c1c4565c1373dbdad007325e836e..adb5410659db4736e60b80fe40ed33bdb8a36569 100644 GIT binary patch literal 879 zcmV-#1Cab5iwFP!00000|E*O^&YL+5+vgNLf~ZWU={-uZRh@@{9n+0F|!Hs zU?`d<^|4r3*@~vvH~cga1~nF3blTtId%~;9Z^lZYyMPgU6%y^bC#-?wK`knWK1b5b zp>*fjWTJ)&tKoc5Z2Ra2yvP||TMq5Or3etR;f-3abvLDjE}^PE9EsMaapvVF_@EGp z+4okAKDBH3Y~\$ey(8%lub@PhZ_C;z0e0;6 zrMV6?O7#bIX!O?!xoo;wR)+2CL#&&&=7ZYqrbS*Od3Oy(oGsS@PO18bi=AcD^3a3@ zOH!QE&%HC>S?`0gI_p}HoJea*_uVXort?YgOFg~TxXxl{ttG1j(RE=J4RV~3dQi4l zVaK`3u}>aQnoG?&>u4P@56Z7iwCuL(yaDw)EUj~GEm(|i6u%%0@E~Y\$K;gc}R^Cg! z7qvk=C~h|r*LL+|8si7Zo?yQ1s)7eK\$?T9U2-Zf;_S^8D2~&pqWP)Fsc_h}lfU?F_xG`2u2U#Y3lLdB{(y5(tS3W3E zq2?@6@}P<7RBTl&C7\$T!c~Ch5GM7>9)-y+~(5Z)p5\$=NDT&ymAq`M?89RF%6 znGaXiLO?#Dc9<=yfBpC;e|`J@qyGNuXMHvAU9)qEviAm_nyxT86W_aHZ{GifTP63j ze_voS;%J}jPertHt+DjszE(PIZMuRJuq&xG)g^H3ap!ZoxRbz1@fd74b(>w#OHQWr z_9lCy^u@CTVd}`%)7i73iYEt&)G|`mgUWR-lw&B@wtKHm^{yeK}E-5TdWxNmgO^\$S z0nRM+&zsEf-y`Lu&t<@8y2X84~>{1-I^f`S?c F0091<#H0WK literal 367 zcmV-#0g(P5iwFP!00000|1FZcv0ym}1^pMrguovZ4hXO}e`_^!pFF58RHs2JefCPP z1{9\$Nvfp#F!HO^Z\$^S0@%\$^kYp\$j4;cT9&T5g`zc%8LTOvlbaK@E9FxeTCbCQ*DxZD}Pj6^D5#xX=GwI#>Gh> z4&cq-A1j|6-qMs{A!xbLyiW*d7XI_)KX4p?qROppx8gNeqlKIBRDG0s={(t_FU50v zLLG(1M^7}tN3}-cIPUQ67j9>{*n#M_<-XHe9ujiqr1^?)n@%Bl#}LRMEzsoB;l) N{{fRy3loL{005Ugvrqs4 -- 2.26.2