From 67e21af2810b6290d77b7b1e1acab92fe52c7a87 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sat, 20 Jan 2024 08:25:39 -0800 Subject: [PATCH] Remove {:opaque} attribute from lemmas --- src/Collections/Sequences/Seq.dfy | 8 ++++---- src/dafny/Collections/Seqs.dfy | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 63d818ae..756102fc 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -653,7 +653,7 @@ module {:options "-functionSyntax:4"} Seq { /* Applying a function to a sequence is distributive over concatenation. That is, concatenating two sequences and then applying Map is the same as applying Map to each sequence separately, and then concatenating the two resulting sequences. */ - lemma {:opaque} LemmaMapDistributesOverConcat(f: (T ~> R), xs: seq, ys: seq) + lemma LemmaMapDistributesOverConcat(f: (T ~> R), xs: seq, ys: seq) requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i]) requires forall j :: 0 <= j < |ys| ==> f.requires(ys[j]) ensures Map(f, xs + ys) == Map(f, xs) + Map(f, ys) @@ -688,7 +688,7 @@ module {:options "-functionSyntax:4"} Seq { /* Filtering a sequence is distributive over concatenation. That is, concatenating two sequences and then using "Filter" is the same as using "Filter" on each sequence separately, and then concatenating the two resulting sequences. */ - lemma {:opaque} LemmaFilterDistributesOverConcat(f: (T ~> bool), xs: seq, ys: seq) + lemma LemmaFilterDistributesOverConcat(f: (T ~> bool), xs: seq, ys: seq) requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i]) requires forall j :: 0 <= j < |ys| ==> f.requires(ys[j]) ensures Filter(f, xs + ys) == Filter(f, xs) + Filter(f, ys) @@ -720,7 +720,7 @@ module {:options "-functionSyntax:4"} Seq { /* Folding to the left is distributive over concatenation. That is, concatenating two sequences and then folding them to the left, is the same as folding to the left the first sequence and using the result to fold to the left the second sequence. */ - lemma {:opaque} LemmaFoldLeftDistributesOverConcat(f: (A, T) -> A, init: A, xs: seq, ys: seq) + lemma LemmaFoldLeftDistributesOverConcat(f: (A, T) -> A, init: A, xs: seq, ys: seq) requires 0 <= |xs + ys| ensures FoldLeft(f, init, xs + ys) == FoldLeft(f, FoldLeft(f, init, xs), ys) { @@ -781,7 +781,7 @@ module {:options "-functionSyntax:4"} Seq { /* Folding to the right is (contravariantly) distributive over concatenation. That is, concatenating two sequences and then folding them to the right, is the same as folding to the right the second sequence and using the result to fold to the right the first sequence. */ - lemma {:opaque} LemmaFoldRightDistributesOverConcat(f: (T, A) -> A, init: A, xs: seq, ys: seq) + lemma LemmaFoldRightDistributesOverConcat(f: (T, A) -> A, init: A, xs: seq, ys: seq) requires 0 <= |xs + ys| ensures FoldRight(f, xs + ys, init) == FoldRight(f, xs, FoldRight(f, ys, init)) { diff --git a/src/dafny/Collections/Seqs.dfy b/src/dafny/Collections/Seqs.dfy index b6b41ac0..c9c7814c 100644 --- a/src/dafny/Collections/Seqs.dfy +++ b/src/dafny/Collections/Seqs.dfy @@ -628,7 +628,7 @@ module {:options "-functionSyntax:4"} Dafny.Collections.Seq { /* Applying a function to a sequence is distributive over concatenation. That is, concatenating two sequences and then applying Map is the same as applying Map to each sequence separately, and then concatenating the two resulting sequences. */ - lemma {:opaque} LemmaMapDistributesOverConcat(f: (T ~> R), xs: seq, ys: seq) + lemma LemmaMapDistributesOverConcat(f: (T ~> R), xs: seq, ys: seq) requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i]) requires forall j :: 0 <= j < |ys| ==> f.requires(ys[j]) ensures Map(f, xs + ys) == Map(f, xs) + Map(f, ys) @@ -663,7 +663,7 @@ module {:options "-functionSyntax:4"} Dafny.Collections.Seq { /* Filtering a sequence is distributive over concatenation. That is, concatenating two sequences and then using "Filter" is the same as using "Filter" on each sequence separately, and then concatenating the two resulting sequences. */ - lemma {:opaque} LemmaFilterDistributesOverConcat(f: (T ~> bool), xs: seq, ys: seq) + lemma LemmaFilterDistributesOverConcat(f: (T ~> bool), xs: seq, ys: seq) requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i]) requires forall j :: 0 <= j < |ys| ==> f.requires(ys[j]) ensures Filter(f, xs + ys) == Filter(f, xs) + Filter(f, ys) @@ -695,7 +695,7 @@ module {:options "-functionSyntax:4"} Dafny.Collections.Seq { /* Folding to the left is distributive over concatenation. That is, concatenating two sequences and then folding them to the left, is the same as folding to the left the first sequence and using the result to fold to the left the second sequence. */ - lemma {:opaque} LemmaFoldLeftDistributesOverConcat(f: (A, T) -> A, init: A, xs: seq, ys: seq) + lemma LemmaFoldLeftDistributesOverConcat(f: (A, T) -> A, init: A, xs: seq, ys: seq) requires 0 <= |xs + ys| ensures FoldLeft(f, init, xs + ys) == FoldLeft(f, FoldLeft(f, init, xs), ys) { @@ -756,7 +756,7 @@ module {:options "-functionSyntax:4"} Dafny.Collections.Seq { /* Folding to the right is (contravariantly) distributive over concatenation. That is, concatenating two sequences and then folding them to the right, is the same as folding to the right the second sequence and using the result to fold to the right the first sequence. */ - lemma {:opaque} LemmaFoldRightDistributesOverConcat(f: (T, A) -> A, init: A, xs: seq, ys: seq) + lemma LemmaFoldRightDistributesOverConcat(f: (T, A) -> A, init: A, xs: seq, ys: seq) requires 0 <= |xs + ys| ensures FoldRight(f, xs + ys, init) == FoldRight(f, xs, FoldRight(f, ys, init)) {