HaRe-0.6: tools/hs2alfa/tests/SortProperties.alfa
--#include "Sort.alfa"
--#include "Alfa/PropositionalCalculus.alfa"
--#include "PreludeProperties.alfa"
{- Error: Error in the definition of LteAllTrans because:
Type does not contain constructor: List A in :-}
package SortProperties where
open Propositional
use Prop, Absurdity, AbsurdityElim, Triviality, TrivialityIntro,
Pred, And, AndIntro, AndElimCont, Implies, ImpliesIntro,
ImpliesElim, Not
open Module_Sort use insert, sort
open Module_Prelude use List, Bool, Ord, (<=)
open PreludeProperties
use IsTrue, AllElems, TotalOrder, ifProp, IsLte, trans,
antisym
-- The property that x is less than or equal to all elements of the list xs:
LteAll (A::Star)(ordA::Ord A)(x::A)(xs::List A) :: Prop
= AllElems A (IsLte A ordA x) xs
-- The property that a lists is ordered:
IsOrdered (A::Star)(ordA::Ord A)(xs::List A) :: Prop
= case xs of {
(Nil) -> Triviality;
(Cons x1 xs') -> And (LteAll A ordA x1 xs') (IsOrdered A ordA xs');}
-- If x1<=x2 and x2 is lte all elements of xs then x1 is lte all elements of xs:
LteAllTrans (A::Star)
(ordA::Ord A)
(x1::A)
(x2::A)
(xs::List A)
(totord::TotalOrder A ordA)
(lt1::IsLte A ordA x1 x2)
(lta::LteAll A ordA x2 xs)
:: LteAll A ordA x1 xs
= case xs of {
(Nil) ->
let ndgoal :: LteAll A ordA x1 Nil@_
= TrivialityIntro
in ndgoal;
(Cons x1' x2') ->
let ndgoal :: LteAll A ordA x1 (Cons@_ x1' x2')
= AndElimCont (IsLte A ordA x2 x1')
(AllElems A (IsLte A ordA x2) x2')
(LteAll A ordA x1 (Cons@_ x1' x2'))
(let ndgoal
:: And (IsLte A ordA x2 x1')
(AllElems A (IsLte A ordA x2) x2')
= lta
in ndgoal)
(\(a::IsLte A ordA x2 x1') ->
\(b::AllElems A (IsLte A ordA x2) x2') ->
let ndgoal :: LteAll A ordA x1 (Cons@_ x1' x2')
= AndIntro (IsLte A ordA x1 x1')
(AllElems A (IsLte A ordA x1) x2')
(let ndgoal :: IsLte A ordA x1 x1'
= trans A ordA totord x1 x2 x1'
(let ndgoal :: IsLte A ordA x1 x2
= lt1
in ndgoal)
(let ndgoal :: IsLte A ordA x2 x1'
= a
in ndgoal)
in ndgoal)
(let ndgoal :: AllElems A (IsLte A ordA x1) x2'
= LteAllTrans A ordA x1 x2 x2' totord
(let ndgoal :: IsLte A ordA x1 x2
= lt1
in ndgoal)
(let ndgoal :: LteAll A ordA x2 x2'
= b
in ndgoal)
in ndgoal)
in ndgoal)
in ndgoal;}
-- If x1 is lte x2 and x2 is lte all elements of xs, then x1 is lte all elements of x2:xs
LteFirst (A::Star)
(ordA::Ord A)
(x1::A)
(x2::A)
(xs::List A)
(totord::TotalOrder A ordA)
(x1p::IsLte A ordA x1 x2)
(x2p::LteAll A ordA x2 xs)
:: LteAll A ordA x1 (Cons@_ x2 xs)
= let ndgoal :: LteAll A ordA x1 (Cons@_ x2 xs)
= AndIntro (IsLte A ordA x1 x2) (AllElems A (IsLte A ordA x1) xs)
(let ndgoal :: IsLte A ordA x1 x2
= x1p
in ndgoal)
(let ndgoal :: LteAll A ordA x1 xs
= LteAllTrans A ordA x1 x2 xs totord
(let ndgoal :: IsLte A ordA x1 x2
= x1p
in ndgoal)
(let ndgoal :: LteAll A ordA x2 xs
= x2p
in ndgoal)
in ndgoal)
in ndgoal
insertLemma (A::Star)
(ordA::Ord A)
(x1::A)
(x2::A)
(xs::List A)
(x1x2::IsLte A ordA x1 x2)
(x1xs::LteAll A ordA x1 xs)
:: LteAll A ordA x1 (insert A ordA x2 xs)
= case xs of {
(Nil) ->
let ndgoal :: LteAll A ordA x1 (insert A ordA x2 Nil@_)
= AndIntro (IsLte A ordA x1 x2)
(AllElems A (IsLte A ordA x1) Nil@_)
(let ndgoal :: IsLte A ordA x1 x2
= x1x2
in ndgoal)
(let ndgoal :: AllElems A (IsLte A ordA x1) Nil@_
= TrivialityIntro
in ndgoal)
in ndgoal;
(Cons x1' x2') ->
let ndgoal :: LteAll A ordA x1 (insert A ordA x2 (Cons@_ x1' x2'))
= ifProp (List A) ((<=) A ordA x2 x1')
(Cons@_ x2 (Cons@_ x1' x2'))
(Cons@_ x1' (insert A ordA x2 x2'))
(\(h::List A) -> LteAll A ordA x1 h)
(\(h::IsLte A ordA x2 x1') ->
let ndgoal :: LteAll A ordA x1 (Cons@_ x2 (Cons@_ x1' x2'))
= AndIntro (IsLte A ordA x1 x2)
(AllElems A (IsLte A ordA x1) (Cons@_ x1' x2'))
(let ndgoal :: IsLte A ordA x1 x2
= x1x2
in ndgoal)
(let ndgoal
:: AllElems A (IsLte A ordA x1)
(Cons@_ x1' x2')
= x1xs
in ndgoal)
in ndgoal)
(\(h::Not (IsLte A ordA x2 x1')) ->
let ndgoal
:: LteAll A ordA x1
(Cons@_ x1' (insert A ordA x2 x2'))
= AndElimCont (IsLte A ordA x1 x1')
(AllElems A (IsLte A ordA x1) x2')
(LteAll A ordA x1
(Cons@_ x1' (insert A ordA x2 x2')))
(let ndgoal
:: And (IsLte A ordA x1 x1')
(AllElems A (IsLte A ordA x1) x2')
= x1xs
in ndgoal)
(\(a::IsLte A ordA x1 x1') ->
\(b::AllElems A (IsLte A ordA x1) x2') ->
let ndgoal
:: LteAll A ordA x1
(Cons@_ x1' (insert A ordA x2 x2'))
= AndIntro (IsLte A ordA x1 x1')
(AllElems A (IsLte A ordA x1)
(insert A ordA x2 x2'))
(let ndgoal :: IsLte A ordA x1 x1'
= a
in ndgoal)
(let ndgoal
:: AllElems A (IsLte A ordA x1)
(insert A ordA x2 x2')
= insertLemma A ordA x1 x2 x2'
(let ndgoal
:: IsLte A ordA x1
x2
= x1x2
in ndgoal)
(let ndgoal
:: LteAll A ordA x1
x2'
= b
in ndgoal)
in ndgoal)
in ndgoal)
in ndgoal)
in ndgoal;}
-- Inserting an element in an ordered lists yields and ordered list:
insertProp (A::Star)
(ordA::Ord A)
(totord::TotalOrder A ordA)
(x::A)
(xs::List A)
(pxs::IsOrdered A ordA xs)
:: IsOrdered A ordA (insert A ordA x xs)
= case xs of {
(Nil) ->
let ndgoal :: IsOrdered A ordA (insert A ordA x Nil@_)
= AndIntro (LteAll A ordA x Nil@_) (IsOrdered A ordA Nil@_)
(let ndgoal :: LteAll A ordA x Nil@_
= TrivialityIntro
in ndgoal)
(let ndgoal :: IsOrdered A ordA Nil@_
= TrivialityIntro
in ndgoal)
in ndgoal;
(Cons x1 x2) ->
let ndgoal :: IsOrdered A ordA (insert A ordA x (Cons@_ x1 x2))
= AndElimCont (LteAll A ordA x1 x2) (IsOrdered A ordA x2)
(IsOrdered A ordA (insert A ordA x (Cons@_ x1 x2)))
(let ndgoal
:: And (LteAll A ordA x1 x2) (IsOrdered A ordA x2)
= pxs
in ndgoal)
(\(a::LteAll A ordA x1 x2) ->
\(b::IsOrdered A ordA x2) ->
let ndgoal
:: IsOrdered A ordA (insert A ordA x (Cons@_ x1 x2))
= ifProp (List A) ((<=) A ordA x x1)
(Cons@_ x (Cons@_ x1 x2))
(Cons@_ x1 (insert A ordA x x2))
(\(h::List A) -> IsOrdered A ordA h)
(\(h::IsLte A ordA x x1) ->
let ndgoal
:: IsOrdered A ordA
(Cons@_ x (Cons@_ x1 x2))
= AndIntro (LteAll A ordA x (Cons@_ x1 x2))
(IsOrdered A ordA (Cons@_ x1 x2))
(let ndgoal
:: LteAll A ordA x
(Cons@_ x1 x2)
= LteFirst A ordA x x1 x2
totord
(let ndgoal
:: IsLte A ordA x x1
= h
in ndgoal)
(let ndgoal
:: LteAll A ordA x1
x2
= a
in ndgoal)
in ndgoal)
(let ndgoal
:: IsOrdered A ordA
(Cons@_ x1 x2)
= pxs
in ndgoal)
in ndgoal)
(\(h::Not (IsLte A ordA x x1)) ->
let ndgoal
:: IsOrdered A ordA
(Cons@_ x1 (insert A ordA x x2))
= AndIntro
(LteAll A ordA x1 (insert A ordA x x2))
(IsOrdered A ordA (insert A ordA x x2))
(let ndgoal
:: LteAll A ordA x1
(insert A ordA x x2)
= insertLemma A ordA x1 x x2
(let ndgoal
:: IsLte A ordA x1 x
= antisym A ordA
totord
x
x1
(let ndgoal
:: Not
(IsLte
A
ordA
x
x1)
= h
in ndgoal)
in ndgoal)
(let ndgoal
:: LteAll A ordA x1
x2
= a
in ndgoal)
in ndgoal)
(let ndgoal
:: IsOrdered A ordA
(insert A ordA x x2)
= insertProp A ordA totord x x2
(let ndgoal
:: IsOrdered A ordA
x2
= b
in ndgoal)
in ndgoal)
in ndgoal)
in ndgoal)
in ndgoal;}
-- The output of the sort function is an ordered list:
sortProp (A::Star)(ordA::Ord A)(totord::TotalOrder A ordA)(xs::List A)
:: IsOrdered A ordA (sort A ordA xs)
= case xs of {
(Nil) ->
let ndgoal :: IsOrdered A ordA (sort A ordA Nil@_)
= TrivialityIntro
in ndgoal;
(Cons x1 x2) ->
let ndgoal :: IsOrdered A ordA (sort A ordA (Cons@_ x1 x2))
= insertProp A ordA totord x1 (sort A ordA x2)
(sortProp A ordA totord x2)
in ndgoal;}
{-# GF Eng IsOrdered A ordA xs = mkSent (xs.s!pnv++["is ordered by"]++ordA.s!pnv) #-}
{-# Alfa hiding on
var "IsOrderedCons" hide 2
var "IsOrdered" hide 2
var "ifProp" hide 5
var "AllElems" hide 1
var "LteAll" hide 2
var "LteFirst" hide 6
var "insertProp" hide 5
var "insertLemma" hide 5
var "AntiSymmetry" hide 1
var "LteAllTrans" hide 6
var "sortProp" hide 3
#-}