I have natural number list l1: [a1,a2,a3 ..an] which undergoes a test condition in the form of function f( m n o:nat l:list nat). As a result some elements get drop and get valid list l2:[b1,b2..bn]. Any element of l1 which follows the condition must present in l2.
Any x of l1 (In x l1) during simplification get this form x=a1\/In x l1.. i have problem in identifying first element.
because after test result (in l2) it has different name or may be drop. How to identify it? Use any other function instead of In x l1?
Sorry, what exactly are you trying to prove? I'm having trouble understanding your use case - you have a list that is filtered on some condition and you get a new list with only the elements that satisfy the condition - are you trying to prove that any element that satisfies the condition must be in the new list? or do you mean something else
Again @pianke, try to provide valid Coq code with your question. Is your problem that you are trying to prove this?
Require Import List. Import ListNotations. Parameter f : list nat -> list nat. Parameter check : nat -> bool. Goal forall x l, In x l -> check x = true -> In x (f l).
Last updated: Oct 04 2023 at 22:01 UTC