LINUX.ORG.RU

История изменений

Исправление AndreyKl, (текущая версия) :

В общем то сама спека не сложная... как бы..
(код на Коке)

Fixpoint argmax (default : nat) (f : nat -> nat) (xs : list nat) : nat :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (s r : nat) (f : nat -> nat) (xs : list nat) : nat :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.


Theorem argmax_correct (d : nat) (f : nat -> nat) (xs : list nat) (x : nat): 
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.

В коде выше
\/ - дизъюнкция
/\ - конъюнкция

Т.е. говоря словами, argmax_correct выражает тот факт что если argmax от d f xs равно какому то x, то либо xs пустой список и тогда x = d, либо сущетсвует такой индекс ix, что x стоит на месте ix в массиве xs и для любого y стоящего на месте iy в массиве xs выполняется следующее: либо f y < f x либо ix <= iy.

Но на доказательстве я что то поплыл. Может как то кривовато сформулировал...

Исправление AndreyKl, :

В общем то сама спека не сложная... как бы..
(код на Коке)

Fixpoint argmax (default : nat) (f : nat -> nat) (xs : list nat) : nat :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (s r : nat) (f : nat -> nat) (xs : list nat) : nat :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.


Theorem argmax_correct (d : nat) (f : nat -> nat) (xs : list nat) (x : nat): 
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.


В коде выше
\/ - дизъюнкция
/\ - конъюнкция


Т.е. говоря словами, argmax_correct выражает тот факт что если argmax от d f xs равно какому то x, то либо xs пустой список и тогда x = d, либо сущетсвует такой индекс ix, что x стоит на месте ix в массиве xs и для любого y стоящего на месте iy в массиве xs выполняется следующее: либо f y < f x либо ix <= iy.

Но на доказательстве я что то поплыл. Может как то кривовато сформулировал...

Исправление AndreyKl, :

В общем то сама спека не сложная... как бы..
(код на Коке)

Fixpoint argmax (default : nat) (f : nat -> nat) (xs : list nat) : nat :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (s r : nat) (f : nat -> nat) (xs : list nat) : nat :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.


Theorem argmax_correct : forall (d : nat) (f : nat -> nat) (xs : list nat) (x : nat),
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.


Т.е. говоря словами, argmax_correct выражает тот факт что если argmax от d f xs равно какому то x, то либо (\/ - дизъюнкция) xs пустой список и (/\ - конъюнкция) тогда x = d, либо сущетсвует такой индекс ix, что x стоит на месте ix в массиве xs и для любого y стоящего на месте iy в массиве xs выполняется следующее: либо f y < f x либо ix <= iy.

Но на доказательстве я что то поплыл. Может как то кривовато сформулировал...

Исправление AndreyKl, :

В общем то сама спека не сложная... как бы..

Fixpoint argmax (default : nat) (f : nat -> nat) (xs : list nat) : nat :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (s r : nat) (f : nat -> nat) (xs : list nat) : nat :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.


Theorem argmax_correct : forall (d : nat) (f : nat -> nat) (xs : list nat) (x : nat),
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.


Т.е. говоря словами, argmax_correct выражает тот факт что если argmax от d f xs равно какому то x, то либо (\/ - дизъюнкция) xs пустой список и (/\ - конъюнкция) тогда x = d, либо сущетсвует такой индекс ix, что x стоит на месте ix в массиве xs и для любого y стоящего на месте iy в массиве xs выполняется следующее: либо f y < f x либо ix <= iy.

Но на доказательстве я что то поплыл. Может как то кривовато сформулировал...

Исходная версия AndreyKl, :

В общем то сама спека не сложная... как бы..

Fixpoint argmax (default : nat) (f : nat -> nat) (xs : list nat) : nat :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (s r : nat) (f : nat -> nat) (xs : list nat) : nat :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.


Theorem argmax_correct : forall (d : nat) (f : nat -> nat) (xs : list nat) (x : nat),
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.


Т.е. говоря словами, argmax_correct выражает тот факт что если argmax от d f xs равно какому то x, то либо (\/ - дизъюнкция) xs пустой список и (/\ - конъюнкция) тогда x = d, либо сущетсвует такой индекс xi, что x стоит на месте xi в массиве xs и для любого y стоящего на месте yi в массиве xs выполняется следующее: либо f y < f x либо ix <= iy.